Grace/Cumulus/Geometry/Euclid/Motions.g17

Open in Workbench Download source

Imports

Geometry.Vectors3 · Algebra.Group.Homomorphism

Declarations

Source

1-- The orientation-preserving isometries of ℝ³ as the bundled group of2-- pairs (M, t) acting by x ↦ M x + t, with SO3 embedded compatibly3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Euclid.Motions9import Geometry.Vectors310import Algebra.Group.Homomorphism1112-- Vector addition.13defgraph addVector (u v : Set) (i ∈ 3) : ℝ := (u(i):R) + (v(i):R)14requires vectorU : u : 3 → ℝ15requires vectorV : v : 3 → ℝ16proof17  have ui := vector.component_real at u, i with vectorU, member18  have vi := vector.component_real at v, i with vectorV, member19  typecheck2021instance addVector.vector (u v : Set)22  requires vectorU : u : 3 → ℝ23  requires vectorV : v : 3 → ℝ24  shows addVector(u, v) : 3 → ℝ25proof26  exact addVector.function with vectorU, vectorV2728theorem addVector.entry (u v i : Set)29  requires vectorU : u : 3 → ℝ30  requires vectorV : v : 3 → ℝ31  requires index : i ∈ 332  shows addVector(u, v)(i) = (u(i):R) + (v(i):R)33proof34  exact addVector.value with vectorU, vectorV, index3536-- Vector addition is associative, has the zero vector as its unit, and37-- cancels against negation.38theorem addVector.assoc (u v w : Set)39  requires vectorU : u : 3 → ℝ40  requires vectorV : v : 3 → ℝ41  requires vectorW : w : 3 → ℝ42  shows addVector(addVector(u, v), w) = addVector(u, addVector(v, w))43proof44  have inner := addVector.vector with vectorU, vectorV45  have inner2 := addVector.vector with vectorV, vectorW46  have left := addVector.vector with inner, vectorW47  have right := addVector.vector with vectorU, inner248  apply FunctionBetween.ext with left, right49  intros i hi50  have ui := vector.component_real at u, i with vectorU, hi51  have vi := vector.component_real at v, i with vectorV, hi52  have wi := vector.component_real at w, i with vectorW, hi53  have e1 := addVector.entry at addVector(u, v), w, i with inner, vectorW, hi54  have e2 := addVector.entry at u, v, i with vectorU, vectorV, hi55  have e3 := addVector.entry at u, addVector(v, w), i with vectorU, inner2, hi56  have e4 := addVector.entry at v, w, i with vectorV, vectorW, hi57  rw [e1, e2, e3, e4]58  ring5960theorem addVector.comm (u v : Set)61  requires vectorU : u : 3 → ℝ62  requires vectorV : v : 3 → ℝ63  shows addVector(u, v) = addVector(v, u)64proof65  have left := addVector.vector with vectorU, vectorV66  have right := addVector.vector with vectorV, vectorU67  apply FunctionBetween.ext with left, right68  intros i hi69  have ui := vector.component_real at u, i with vectorU, hi70  have vi := vector.component_real at v, i with vectorV, hi71  have e1 := addVector.entry at u, v, i with vectorU, vectorV, hi72  have e2 := addVector.entry at v, u, i with vectorV, vectorU, hi73  rw [e1, e2]74  ring7576theorem addVector.zero (u : Set)77  requires vectorU : u : 3 → ℝ78  shows addVector(u, zeroVector) = u79proof80  have zero := zeroVector.vector81  have sum := addVector.vector with vectorU, zero82  apply FunctionBetween.ext with sum, vectorU83  intros i hi84  have ui := vector.component_real at u, i with vectorU, hi85  have e1 := addVector.entry at u, zeroVector, i with vectorU, zero, hi86  have e2 := zeroVector.entry at i with hi87  rw [e1, e2]88  ring8990theorem addVector.zero_left (u : Set)91  requires vectorU : u : 3 → ℝ92  shows addVector(zeroVector, u) = u93proof94  have zero := zeroVector.vector95  have sum := addVector.vector with zero, vectorU96  apply FunctionBetween.ext with sum, vectorU97  intros i hi98  have ui := vector.component_real at u, i with vectorU, hi99  have e1 := addVector.entry at zeroVector, u, i with zero, vectorU, hi100  have e2 := zeroVector.entry at i with hi101  rw [e1, e2]102  ring103104theorem addVector.neg (u : Set)105  requires vectorU : u : 3 → ℝ106  shows addVector(u, vectorNeg(u)) = zeroVector107proof108  have zero := zeroVector.vector109  have negated := vectorNeg.vector with vectorU110  have sum := addVector.vector with vectorU, negated111  apply FunctionBetween.ext with sum, zero112  intros i hi113  have ui := vector.component_real at u, i with vectorU, hi114  have e1 := addVector.entry at u, vectorNeg(u), i with vectorU, negated, hi115  have e2 := vectorNeg.entry at u, i with vectorU, hi116  have e3 := zeroVector.entry at i with hi117  rw [e1, e2, e3]118  ring119120theorem addVector.neg_left (u : Set)121  requires vectorU : u : 3 → ℝ122  shows addVector(vectorNeg(u), u) = zeroVector123proof124  have zero := zeroVector.vector125  have negated := vectorNeg.vector with vectorU126  have sum := addVector.vector with negated, vectorU127  apply FunctionBetween.ext with sum, zero128  intros i hi129  have ui := vector.component_real at u, i with vectorU, hi130  have e1 := addVector.entry at vectorNeg(u), u, i with negated, vectorU, hi131  have e2 := vectorNeg.entry at u, i with vectorU, hi132  have e3 := zeroVector.entry at i with hi133  rw [e1, e2, e3]134  ring135136-- A matrix acts linearly: it respects sums, the zero vector, and negation.137theorem matrixVector.add_vector (M : realRing ^ 3 × 3) (u v : Set)138  requires vectorU : u : 3 → ℝ139  requires vectorV : v : 3 → ℝ140  shows M · addVector(u, v) = addVector(M · u, M · v)141proof142  have sum := addVector.vector with vectorU, vectorV143  have left := matrixVector.vector at M, addVector(u, v) with *144  have imageU := matrixVector.vector at M, u with *145  have imageV := matrixVector.vector at M, v with *146  have right := addVector.vector with imageU, imageV147  apply FunctionBetween.ext with left, right148  intros i hi149  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi150  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem151  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem152  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem153  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem154  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem155  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem156  have e1 := matrixVector.entry at M, addVector(u, v), i with *157  have e2 := addVector.entry at M · u, M · v, i with imageU, imageV, hi158  have e3 := matrixVector.entry at M, u, i with *159  have e4 := matrixVector.entry at M, v, i with *160  have s0 := addVector.entry at u, v, 0 with vectorU, vectorV, index.zero_mem161  have s1 := addVector.entry at u, v, 1 with vectorU, vectorV, index.one_mem162  have s2 := addVector.entry at u, v, 2 with vectorU, vectorV, index.two_mem163  rw [e1, e2, e3, e4, s0, s1, s2]164  ring165166theorem matrixVector.zero_vector (M : realRing ^ 3 × 3)167  shows M · zeroVector = zeroVector168proof169  have zero := zeroVector.vector170  have left := matrixVector.vector at M, zeroVector with *171  apply FunctionBetween.ext with left, zero172  intros i hi173  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi174  have e1 := matrixVector.entry at M, zeroVector, i with *175  have z0 := zeroVector.entry at 0 with index.zero_mem176  have z1 := zeroVector.entry at 1 with index.one_mem177  have z2 := zeroVector.entry at 2 with index.two_mem178  have zi := zeroVector.entry at i with hi179  rw [e1, z0, z1, z2, zi]180  ring181182-- The product in SO3 is the matrix product.183theorem SO3.product_value (M N : realRing ^ 3 × 3)184  requires hM : M ∈ so3Matrices185  requires hN : N ∈ so3Matrices186  shows call2(Group.mul(SO3), M, N) = M * N187proof188  have ring := matrixRing.real_ring189  have magma := IsSemigroup.magma with190    (IsMonoid.semigroup with (IsRing.multiplicative with (Ring.parts191        with ring)))192  have closedMul : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))193    intros A hA B hB194    have matrixA := so3Matrices.matrix with hA195    have matrixB := so3Matrices.matrix with hB196    exact so3Matrices.mul_mem with *197  have operation := restrictBinary.value at Ring.carrier(matrixRing(realRing,198      3)),199    so3Matrices, Ring.mul(matrixRing(realRing, 3)), M, N200    with magma, so3Matrices.subset, closedMul, hM, hN201  rw SO3.mulOf202  exact operation203204-- The motions: a rotation paired with a translation vector.205def motions : Set := so3Matrices × ℝ³206207theorem motions.pair (M t : Set)208  requires hM : M ∈ so3Matrices209  requires ht : t ∈ ℝ³210  shows (M, t) ∈ motions211proof212  unfold motions213  exact product.pair with hM, ht214215theorem motions.cases (p : Set)216  requires hp : p ∈ motions217  shows ∃ M ∈ so3Matrices, ∃ t ∈ ℝ³, p = (M, t)218proof219  unfold motions at hp220  obtain ⟨bound, M, hM, t, ht, shape⟩ := product.membership.forward with hp221  exact ⟨M, hM, t, ht, shape⟩222223-- The product (M, t) · (N, s) = (M N, M s + t), the unit (1, 0), and the224-- inverse (Mᵀ, −Mᵀ t).225defgraph motionMul (q ∈ motions × motions) : motions :=226  (call2(Ring.mul(matrixRing(realRing, 3)), fst(fst(q)), fst(snd(q))),227    addVector(fst(fst(q)) · snd(snd(q)), snd(fst(q))))228proof229  obtain ⟨bound, p, hp, r, hr, shape⟩ :=230    product.membership.forward with member231  obtain ⟨M, hM, t, ht, pShape⟩ := motions.cases with hp232  obtain ⟨N, hN, s, hs, rShape⟩ := motions.cases with hr233  have matrixM := so3Matrices.matrix with hM234  have matrixN := so3Matrices.matrix with hN235  have productIn := so3Matrices.mul_mem with hM, hN236  have vectorT := ℝ³.function with ht237  have vectorS := ℝ³.function with hs238  have image := matrixVector.vector at M, s with *239  have sum := addVector.vector with image, vectorT240  have sumIn := ℝ³.of_function with sum241  have outerFirst := fst.pair at (M, t), (N, s)242  have outerSecond := snd.pair at (M, t), (N, s)243  have firstP := fst.pair at M, t244  have secondP := snd.pair at M, t245  have firstR := fst.pair at N, s246  have secondR := snd.pair at N, s247  rw [shape, pShape, rShape, outerFirst, outerSecond, firstP, secondP, firstR,248      secondR]249  exact motions.pair with productIn, sumIn250251def motionOne : Set := (matrixRing(realRing, 3)[1], zeroVector)252253theorem motionOne.graph254  shows motionOne = (matrixRing(realRing, 3)[1], zeroVector)255proof256  simp [motionOne]257258theorem motionOne.member259  shows motionOne ∈ motions260proof261  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector262  rw motionOne.graph263  exact motions.pair with so3Matrices.one_mem, zeroIn264265defgraph motionInv (p ∈ motions) : motions :=266  (transpose(fst(p)), vectorNeg(transpose(fst(p)) · snd(p)))267proof268  obtain ⟨M, hM, t, ht, shape⟩ := motions.cases with member269  have matrixM := so3Matrices.matrix with hM270  have transposedIn := so3Matrices.transpose_mem with hM271  have transposed := transpose.matrix at M with *272  have vectorT := ℝ³.function with ht273  have image := matrixVector.vector at transpose(M), t with *274  have negated := vectorNeg.vector with image275  have negIn := ℝ³.of_function with negated276  have firstP := fst.pair at M, t277  have secondP := snd.pair at M, t278  rw [shape, firstP, secondP]279  exact motions.pair with transposedIn, negIn280281theorem motionMul.apply (M N : realRing ^ 3 × 3) (t s : Set)282  requires hM : M ∈ so3Matrices283  requires hN : N ∈ so3Matrices284  requires ht : t ∈ ℝ³285  requires hs : s ∈ ℝ³286  shows motionMul((M, t), (N, s)) = (M * N, addVector(M · s, t))287proof288  have first := motions.pair with hM, ht289  have second := motions.pair with hN, hs290  have pair :=291      product.pair at (M, t), (N, s), motions, motions with first, second292  have value := motionMul.value at ((M, t), (N, s)) with pair293  have outerFirst := fst.pair at (M, t), (N, s)294  have outerSecond := snd.pair at (M, t), (N, s)295  have firstP := fst.pair at M, t296  have secondP := snd.pair at M, t297  have firstR := fst.pair at N, s298  have secondR := snd.pair at N, s299  simp [call2]300301theorem motionInv.apply (M : realRing ^ 3 × 3) (t : Set)302  requires hM : M ∈ so3Matrices303  requires ht : t ∈ ℝ³304  shows motionInv((M, t)) = (transpose(M), vectorNeg(transpose(M) · t))305proof306  have pair := motions.pair with hM, ht307  have value := motionInv.value at (M, t) with pair308  have firstP := fst.pair at M, t309  have secondP := snd.pair at M, t310  rw [value, firstP, secondP]311  rfl312313-- The group laws of the product on explicit pairs.314theorem motionMul.assoc (M N P : realRing ^ 3 × 3) (t s r : Set)315  requires hM : M ∈ so3Matrices316  requires hN : N ∈ so3Matrices317  requires hP : P ∈ so3Matrices318  requires ht : t ∈ ℝ³319  requires hs : s ∈ ℝ³320  requires hr : r ∈ ℝ³321  shows motionMul(motionMul((M, t), (N, s)), (P, r)) =322    motionMul((M, t), motionMul((N, s), (P, r)))323proof324  have productMN := so3Matrices.mul_mem with hM, hN325  have productNP := so3Matrices.mul_mem with hN, hP326  have vectorT := ℝ³.function with ht327  have vectorS := ℝ³.function with hs328  have vectorR := ℝ³.function with hr329  have imageS := matrixVector.vector at M, s with *330  have imageR := matrixVector.vector at N, r with *331  have sumMS : addVector(M · s, t) ∈ ℝ³ :=332    ℝ³.of_function with (addVector.vector with imageS, vectorT)333  have sumNR : addVector(N · r, s) ∈ ℝ³ :=334    ℝ³.of_function with (addVector.vector with imageR, vectorS)335  have first := motionMul.apply with hM, hN, ht, hs336  have second := motionMul.apply at M * N, P, addVector(M · s, t), r with337    productMN, hP, sumMS, hr338  have third := motionMul.apply with hN, hP, hs, hr339  have fourth := motionMul.apply at M, N * P, t, addVector(N · r, s) with340    hM, productNP, ht, sumNR341  have assocMatrix := matrixRing.mul_assoc at M, N, P with *342  have composed := matrixVector.mul at M, N, r with vectorR343  have linear := matrixVector.add_vector at M, N · r, s with imageR, vectorS344  have imageNR := matrixVector.vector at M, N · r with *345  have assocVector := addVector.assoc at M · (N · r), M · s, t with346    imageNR, imageS, vectorT347  rw [first, second, third, fourth, assocMatrix, composed, linear, assocVector]348  rfl349350theorem motionMul.one_left (M : realRing ^ 3 × 3) (t : Set)351  requires hM : M ∈ so3Matrices352  requires ht : t ∈ ℝ³353  shows motionMul(motionOne, (M, t)) = (M, t)354proof355  have one := Matrix.one_matrix356  have oneIn := so3Matrices.one_mem357  have zero := zeroVector.vector358  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zero359  have vectorT := ℝ³.function with ht360  have value := motionMul.apply at matrixRing(realRing, 3)[1], M, zeroVector,361      t with362    oneIn, hM, zeroIn, ht363  have unitMul := matrixRing.one_mul at M with *364  have unitAct := matrixVector.one at t with vectorT365  have unitAdd := addVector.zero at t with vectorT366  rw [motionOne.graph, value, unitMul, unitAct, unitAdd]367  rfl368369theorem motionMul.one_right (M : realRing ^ 3 × 3) (t : Set)370  requires hM : M ∈ so3Matrices371  requires ht : t ∈ ℝ³372  shows motionMul((M, t), motionOne) = (M, t)373proof374  have one := Matrix.one_matrix375  have oneIn := so3Matrices.one_mem376  have zero := zeroVector.vector377  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zero378  have vectorT := ℝ³.function with ht379  have value := motionMul.apply at M, matrixRing(realRing, 3)[1], t,380      zeroVector with381    hM, oneIn, ht, zeroIn382  have unitMul := matrixRing.mul_one at M with *383  have killed := matrixVector.zero_vector at M with *384  have unitAdd := addVector.zero_left at t with vectorT385  rw [motionOne.graph, value, unitMul, killed, unitAdd]386  rfl387388theorem motionMul.inv_left (M : realRing ^ 3 × 3) (t : Set)389  requires hM : M ∈ so3Matrices390  requires ht : t ∈ ℝ³391  shows motionMul(motionInv((M, t)), (M, t)) = motionOne392proof393  have transposedIn := so3Matrices.transpose_mem with hM394  have transposed := transpose.matrix at M with *395  have vectorT := ℝ³.function with ht396  have imageT := matrixVector.vector at transpose(M), t with *397  have negated := vectorNeg.vector with imageT398  have negIn : vectorNeg(transpose(M) · t) ∈ ℝ³ :=399    ℝ³.of_function with negated400  have invValue := motionInv.apply with hM, ht401  have value := motionMul.apply at transpose(M), M,402      vectorNeg(transpose(M) · t), t with403    transposedIn, hM, negIn, ht404  have orthogonal := Orthogonal.left with (so3Matrices.orthogonal with hM)405  have cancel := addVector.neg at transpose(M) · t with imageT406  rw [invValue, value, orthogonal, cancel, motionOne.graph]407  rfl408409theorem motionMul.inv_right (M : realRing ^ 3 × 3) (t : Set)410  requires hM : M ∈ so3Matrices411  requires ht : t ∈ ℝ³412  shows motionMul((M, t), motionInv((M, t))) = motionOne413proof414  have transposedIn := so3Matrices.transpose_mem with hM415  have transposed := transpose.matrix at M with *416  have vectorT := ℝ³.function with ht417  have imageT := matrixVector.vector at transpose(M), t with *418  have negated := vectorNeg.vector with imageT419  have negIn : vectorNeg(transpose(M) · t) ∈ ℝ³ :=420    ℝ³.of_function with negated421  have invValue := motionInv.apply with hM, ht422  have value := motionMul.apply at M, transpose(M), t,423      vectorNeg(transpose(M) · t) with424    hM, transposedIn, ht, negIn425  have orthogonal := Orthogonal.right with (so3Matrices.orthogonal with hM)426  have negLaw := matrixVector.neg at M, transpose(M) · t with imageT427  have composed := matrixVector.mul at M, transpose(M), t with vectorT428  have unitAct := matrixVector.one at t with vectorT429  have cancel := addVector.neg_left at t with vectorT430  rw [invValue, value, negLaw, ← composed, orthogonal, unitAct, cancel,431      motionOne.graph]432  rfl433434-- The group of motions.435def Motions : Set := Group.mk(motions, motionMul, motionOne, motionInv)436437theorem Motions.carrierOf438  shows Group.carrier(Motions) = motions439proof440  simp [Motions, Group.mk.carrier]441442theorem Motions.mulOf443  shows Group.mul(Motions) = motionMul444proof445  simp [Motions, Group.mk.mul]446447theorem Motions.oneOf448  shows Group.one(Motions) = motionOne449proof450  simp [Motions, Group.mk.one]451452theorem Motions.invOf453  shows Group.inv(Motions) = motionInv454proof455  simp [Motions, Group.mk.inv]456457theorem Motions.engine458  shows IsGroup(motions, motionMul, motionOne, motionInv)459proof460  have magma : IsMagma(motions, motionMul)461    unfold IsMagma462    exact motionMul.function463  have associative : Associative(motions, motionMul)464    unfold Associative465    intros x hx y hy z hz466    obtain ⟨M, hM, t, ht, xShape⟩ := motions.cases with hx467    obtain ⟨N, hN, s, hs, yShape⟩ := motions.cases with hy468    obtain ⟨P, hP, r, hr, zShape⟩ := motions.cases with hz469    have matrixM := so3Matrices.matrix with hM470    have matrixN := so3Matrices.matrix with hN471    have matrixP := so3Matrices.matrix with hP472    rw [xShape, yShape, zShape]473    exact motionMul.assoc with *474  have identity : Identity(motions, motionMul, motionOne)475    unfold Identity476    constructor477    . exact motionOne.member478    . intros x hx479      obtain ⟨M, hM, t, ht, xShape⟩ := motions.cases with hx480      have matrixM := so3Matrices.matrix with hM481      rw xShape482      constructor483      . exact motionMul.one_left with *484      . exact motionMul.one_right with *485  have inverse : Inverse(motions, motionMul, motionOne, motionInv)486    unfold Inverse487    constructor488    . exact motionInv.function489    . intros x hx490      obtain ⟨M, hM, t, ht, xShape⟩ := motions.cases with hx491      have matrixM := so3Matrices.matrix with hM492      rw xShape493      constructor494      . exact motionMul.inv_left with *495      . exact motionMul.inv_right with *496  unfold IsGroup497  exact ⟨⟨⟨magma, associative⟩, identity⟩, inverse⟩498499instance Motions.group500  shows Group(Motions)501proof502  have engine := Motions.engine503  unfold Motions504  exact Group.of_parts with engine505506-- The action of the motions on ℝ³: (M, t) sends x to M x + t.507defgraph motionAction (q ∈ motions × ℝ³) : ℝ³ :=508  addVector(fst(fst(q)) · snd(q), snd(fst(q)))509proof510  obtain ⟨bound, p, hp, x, hx, shape⟩ :=511    product.membership.forward with member512  obtain ⟨M, hM, t, ht, pShape⟩ := motions.cases with hp513  have matrixM := so3Matrices.matrix with hM514  have vectorT := ℝ³.function with ht515  have vectorX := ℝ³.function with hx516  have image := matrixVector.vector at M, x with *517  have sum := addVector.vector with image, vectorT518  have outerFirst := fst.pair at (M, t), x519  have outerSecond := snd.pair at (M, t), x520  have firstP := fst.pair at M, t521  have secondP := snd.pair at M, t522  rw [shape, pShape, outerFirst, outerSecond, firstP, secondP]523  exact ℝ³.of_function with sum524525theorem motionAction.apply (M : realRing ^ 3 × 3) (t x : Set)526  requires hM : M ∈ so3Matrices527  requires ht : t ∈ ℝ³528  requires hx : x ∈ ℝ³529  shows motionAction((M, t), x) = addVector(M · x, t)530proof531  have first := motions.pair with hM, ht532  have pair := product.pair at (M, t), x, motions, ℝ³ with first, hx533  have value := motionAction.value at ((M, t), x) with pair534  have outerFirst := fst.pair at (M, t), x535  have outerSecond := snd.pair at (M, t), x536  have firstP := fst.pair at M, t537  have secondP := snd.pair at M, t538  simp [call2]539540theorem motionAction.action541  shows motionAction : Motions ↷ ℝ³542proof543  have group := Motions.group544  have function := motionAction.function545  rw ← Motions.carrierOf at function546  apply Action.mk with group, function547  . intros x hx548    have vectorX := ℝ³.function with hx549    have one := Matrix.one_matrix550    have oneIn := so3Matrices.one_mem551    have zeroIn : zeroVector ∈ ℝ³ :=552      ℝ³.of_function with zeroVector.vector553    have value := motionAction.apply at matrixRing(realRing, 3)[1],554        zeroVector, x with555      oneIn, zeroIn, hx556    have unitAct := matrixVector.one at x with vectorX557    have unitAdd := addVector.zero at x with vectorX558    rw [Motions.oneOf, motionOne.graph, value, unitAct, unitAdd]559    rfl560  . intros g hg h hh x hx561    rw Motions.carrierOf at hg562    rw Motions.carrierOf at hh563    obtain ⟨M, hM, t, ht, gShape⟩ := motions.cases with hg564    obtain ⟨N, hN, s, hs, hShape⟩ := motions.cases with hh565    have matrixM := so3Matrices.matrix with hM566    have matrixN := so3Matrices.matrix with hN567    have vectorT := ℝ³.function with ht568    have vectorS := ℝ³.function with hs569    have vectorX := ℝ³.function with hx570    have productIn := so3Matrices.mul_mem with hM, hN571    have imageS := matrixVector.vector at M, s with *572    have sumIn : addVector(M · s, t) ∈ ℝ³ :=573      ℝ³.of_function with (addVector.vector with imageS, vectorT)574    have imageX := matrixVector.vector at N, x with *575    have innerIn : addVector(N · x, s) ∈ ℝ³ :=576      ℝ³.of_function with (addVector.vector with imageX, vectorS)577    have product := motionMul.apply with hM, hN, ht, hs578    have outer := motionAction.apply at M * N, addVector(M · s, t), x with579      productIn, sumIn, hx580    have inner := motionAction.apply at N, s, x with hN, hs, hx581    have composed :=582        motionAction.apply at M, t, addVector(N · x, s) with hM, ht, innerIn583    have assocMatrix := matrixVector.mul at M, N, x with vectorX584    have linear := matrixVector.add_vector at M, N · x, s with imageX, vectorS585    have imageNX := matrixVector.vector at M, N · x with *586    have assocVector := addVector.assoc at M · (N · x), M · s, t with587      imageNX, imageS, vectorT588    rw [gShape, hShape, Motions.mulOf, product, outer, inner, composed,589      assocMatrix, linear, assocVector]590    rfl591592-- The rotations as the motions fixing the origin.593defgraph rotationMotion (M ∈ so3Matrices) : motions := (M, zeroVector)594proof595  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector596  exact motions.pair with member, zeroIn597598theorem rotationMotion.apply (M : Set)599  requires hM : M ∈ so3Matrices600  shows rotationMotion(M) = (M, zeroVector)601proof602  exact rotationMotion.value with hM603604theorem rotationMotion.hom605  shows rotationMotion : SO3 →* Motions606proof607  have source := SO3.group608  have target := Motions.group609  have function := rotationMotion.function610  rw [← SO3.carrierOf, ← Motions.carrierOf] at function611  apply GroupHom.mk with source, target, function612  intros M hM N hN613  rw SO3.carrierOf at hM614  rw SO3.carrierOf at hN615  have matrixM := so3Matrices.matrix with hM616  have matrixN := so3Matrices.matrix with hN617  have productIn := so3Matrices.mul_mem with hM, hN618  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector619  have operation := SO3.product_value with hM, hN620  have imageM := rotationMotion.apply with hM621  have imageN := rotationMotion.apply with hN622  have imageMN := rotationMotion.apply with productIn623  have product := motionMul.apply at M, N, zeroVector, zeroVector with hM, hN,624      zeroIn, zeroIn625  have killed := matrixVector.zero_vector at M with *626  have unitAdd := addVector.zero at zeroVector with zeroVector.vector627  rw [operation, imageMN, imageM, imageN, Motions.mulOf, product, killed,628      unitAdd]629  rfl630631-- A rotation acts on ℝ³ as its motion does.632theorem rotationMotion.compatible633  shows ∀ M ∈ Group.carrier(SO3), ∀ x ∈ ℝ³,634    spaceAction(M, x) = motionAction(rotationMotion(M), x)635proof636  intros M hM x hx637  rw SO3.carrierOf at hM638  have matrixM := so3Matrices.matrix with hM639  have vectorX := ℝ³.function with hx640  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector641  have image := rotationMotion.apply with hM642  have space := spaceAction.apply with hM, hx643  have motion := motionAction.apply at M, zeroVector, x with hM, zeroIn, hx644  have imageX := matrixVector.vector at M, x with *645  have unitAdd := addVector.zero at M · x with imageX646  rw [image, space, motion, unitAdd]647  rfl648