Metamath Proof Explorer

Theorem angmgmlem

Description: Lemma for angmgm . (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses angmgmval.p 
|- P = ( Base ` G )
angmgmval.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmgmval.i 
|- I = ( Itv ` G )
angmgmval.d 
|- .- = ( dist ` G )
angmgmval.c 
|- .~ = ( cgrA ` G )
angmgmval.l 
|- L = ( LineG ` G )
angmgmval.o 
|- .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
angmgmval.j 
|- J = ( AngMgm ` G )
angmgmlem.g 
|- ( ph -> G e. TarskiG )
angmgmlem.x 
|- ( ph -> X e. P )
angmgmlem.y 
|- ( ph -> Y e. ( P \ { X } ) )
Assertion angmgmlem 
|- ( ph -> ( J e. Mgm /\ [ <" X Y X "> ] .~ = ( 0g ` J ) ) )

Proof

Step Hyp Ref Expression
1 angmgmval.p 
 |-  P = ( Base ` G )
2 angmgmval.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmgmval.i 
 |-  I = ( Itv ` G )
4 angmgmval.d 
 |-  .- = ( dist ` G )
5 angmgmval.c 
 |-  .~ = ( cgrA ` G )
6 angmgmval.l 
 |-  L = ( LineG ` G )
7 angmgmval.o 
 |-  .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
8 angmgmval.j 
 |-  J = ( AngMgm ` G )
9 angmgmlem.g 
 |-  ( ph -> G e. TarskiG )
10 angmgmlem.x 
 |-  ( ph -> X e. P )
11 angmgmlem.y 
 |-  ( ph -> Y e. ( P \ { X } ) )
12 eqid 
 |-  ( leA ` G ) = ( leA ` G )
13 1 2 3 4 5 6 7 8 12 angmgmval 
 |-  ( G e. TarskiG -> J = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } /s .~ ) )
14 9 13 syl 
 |-  ( ph -> J = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } /s .~ ) )
15 ovex 
 |-  ( P ^m ( 0 ..^ 3 ) ) e. _V
16 2 15 rabex2 
 |-  A e. _V
17 1nn 
 |-  1 e. NN
18 basendx 
 |-  ( Base ` ndx ) = 1
19 1lt2 
 |-  1 < 2
20 2nn 
 |-  2 e. NN
21 plusgndx 
 |-  ( +g ` ndx ) = 2
22 2lt10 
 |-  2 < ; 1 0
23 10nn 
 |-  ; 1 0 e. NN
24 plendx 
 |-  ( le ` ndx ) = ; 1 0
25 17 18 19 20 21 22 23 24 strle3 
 |-  { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } Struct <. 1 , ; 1 0 >.
26 baseid 
 |-  Base = Slot ( Base ` ndx )
27 snsstp1 
 |-  { <. ( Base ` ndx ) , A >. } C_ { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. }
28 25 26 27 strfv 
 |-  ( A e. _V -> A = ( Base ` { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } ) )
29 16 28 mp1i 
 |-  ( ph -> A = ( Base ` { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } ) )
30 5 fvexi 
 |-  .~ e. _V
31 30 a1i 
 |-  ( ph -> .~ e. _V )
32 tpex 
 |-  { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } e. _V
33 32 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } e. _V )
34 1 2 5 9 cgrabasimass 
 |-  ( ph -> ( .~ " A ) C_ A )
35 14 29 31 33 34 qusin 
 |-  ( ph -> J = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } /s ( .~ i^i ( A X. A ) ) ) )
36 16 16 mpoex 
 |-  ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) e. _V
37 7 36 eqeltri 
 |-  .+ e. _V
38 plusgid 
 |-  +g = Slot ( +g ` ndx )
39 snsstp2 
 |-  { <. ( +g ` ndx ) , .+ >. } C_ { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. }
40 25 38 39 strfv 
 |-  ( .+ e. _V -> .+ = ( +g ` { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } ) )
41 37 40 ax-mp 
 |-  .+ = ( +g ` { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , ( leA ` G ) >. } )
42 1 2 5 9 cgraer 
 |-  ( ph -> ( .~ i^i ( A X. A ) ) Er A )
43 9 ad2antrr 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> G e. TarskiG )
44 brinxp2 
 |-  ( a ( .~ i^i ( A X. A ) ) p <-> ( ( a e. A /\ p e. A ) /\ a .~ p ) )
45 44 biimpi 
 |-  ( a ( .~ i^i ( A X. A ) ) p -> ( ( a e. A /\ p e. A ) /\ a .~ p ) )
46 45 ad2antlr 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> ( ( a e. A /\ p e. A ) /\ a .~ p ) )
47 46 simplld 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> a e. A )
48 brinxp2 
 |-  ( b ( .~ i^i ( A X. A ) ) q <-> ( ( b e. A /\ q e. A ) /\ b .~ q ) )
49 48 bilani 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> ( ( b e. A /\ q e. A ) /\ b .~ q ) )
50 49 simplld 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> b e. A )
51 1 2 3 4 5 6 43 7 47 50 angmgmaddcl 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> ( a .+ b ) e. A )
52 46 simplrd 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> p e. A )
53 49 simplrd 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> q e. A )
54 1 2 3 4 5 6 43 7 52 53 angmgmaddcl 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> ( p .+ q ) e. A )
55 46 simprd 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> a .~ p )
56 49 simprd 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> b .~ q )
57 1 2 3 4 5 6 43 7 52 53 47 50 55 56 angmgmaddcpbl 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> ( a .+ b ) .~ ( p .+ q ) )
58 brinxp2 
 |-  ( ( a .+ b ) ( .~ i^i ( A X. A ) ) ( p .+ q ) <-> ( ( ( a .+ b ) e. A /\ ( p .+ q ) e. A ) /\ ( a .+ b ) .~ ( p .+ q ) ) )
59 51 54 57 58 syl21anbrc 
 |-  ( ( ( ph /\ a ( .~ i^i ( A X. A ) ) p ) /\ b ( .~ i^i ( A X. A ) ) q ) -> ( a .+ b ) ( .~ i^i ( A X. A ) ) ( p .+ q ) )
60 59 expl 
 |-  ( ph -> ( ( a ( .~ i^i ( A X. A ) ) p /\ b ( .~ i^i ( A X. A ) ) q ) -> ( a .+ b ) ( .~ i^i ( A X. A ) ) ( p .+ q ) ) )
61 9 3ad2ant1 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> G e. TarskiG )
62 simp2 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> i e. A )
63 simp3 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> j e. A )
64 1 2 3 4 5 6 61 7 62 63 angmgmaddcl 
 |-  ( ( ph /\ i e. A /\ j e. A ) -> ( i .+ j ) e. A )
65 1 fvexi 
 |-  P e. _V
66 65 a1i 
 |-  ( ph -> P e. _V )
67 11 eldifad 
 |-  ( ph -> Y e. P )
68 11 eldifsnbd 
 |-  ( ph -> Y =/= X )
69 68 necomd 
 |-  ( ph -> X =/= Y )
70 2 66 10 67 10 69 68 elcgrabasrd 
 |-  ( ph -> <" X Y X "> e. A )
71 9 adantr 
 |-  ( ( ph /\ i e. A ) -> G e. TarskiG )
72 70 adantr 
 |-  ( ( ph /\ i e. A ) -> <" X Y X "> e. A )
73 simpr 
 |-  ( ( ph /\ i e. A ) -> i e. A )
74 1 2 3 4 5 6 71 7 72 73 angmgmaddcl 
 |-  ( ( ph /\ i e. A ) -> ( <" X Y X "> .+ i ) e. A )
75 10 adantr 
 |-  ( ( ph /\ i e. A ) -> X e. P )
76 11 adantr 
 |-  ( ( ph /\ i e. A ) -> Y e. ( P \ { X } ) )
77 1 2 3 4 5 6 71 7 75 76 73 angmgmaddlid 
 |-  ( ( ph /\ i e. A ) -> ( <" X Y X "> .+ i ) .~ i )
78 brinxp2 
 |-  ( ( <" X Y X "> .+ i ) ( .~ i^i ( A X. A ) ) i <-> ( ( ( <" X Y X "> .+ i ) e. A /\ i e. A ) /\ ( <" X Y X "> .+ i ) .~ i ) )
79 74 73 77 78 syl21anbrc 
 |-  ( ( ph /\ i e. A ) -> ( <" X Y X "> .+ i ) ( .~ i^i ( A X. A ) ) i )
80 1 2 3 4 5 6 71 7 73 72 angmgmaddcl 
 |-  ( ( ph /\ i e. A ) -> ( i .+ <" X Y X "> ) e. A )
81 1 2 3 4 5 6 71 7 75 76 73 angmgmaddrid 
 |-  ( ( ph /\ i e. A ) -> ( i .+ <" X Y X "> ) .~ i )
82 brinxp2 
 |-  ( ( i .+ <" X Y X "> ) ( .~ i^i ( A X. A ) ) i <-> ( ( ( i .+ <" X Y X "> ) e. A /\ i e. A ) /\ ( i .+ <" X Y X "> ) .~ i ) )
83 80 73 81 82 syl21anbrc 
 |-  ( ( ph /\ i e. A ) -> ( i .+ <" X Y X "> ) ( .~ i^i ( A X. A ) ) i )
84 35 29 41 42 33 60 64 70 79 83 qusmgm 
 |-  ( ph -> ( J e. Mgm /\ [ <" X Y X "> ] ( .~ i^i ( A X. A ) ) = ( 0g ` J ) ) )
85 ecinxp 
 |-  ( ( ( .~ " A ) C_ A /\ <" X Y X "> e. A ) -> [ <" X Y X "> ] .~ = [ <" X Y X "> ] ( .~ i^i ( A X. A ) ) )
86 34 70 85 syl2anc 
 |-  ( ph -> [ <" X Y X "> ] .~ = [ <" X Y X "> ] ( .~ i^i ( A X. A ) ) )
87 86 eqeq1d 
 |-  ( ph -> ( [ <" X Y X "> ] .~ = ( 0g ` J ) <-> [ <" X Y X "> ] ( .~ i^i ( A X. A ) ) = ( 0g ` J ) ) )
88 87 anbi2d 
 |-  ( ph -> ( ( J e. Mgm /\ [ <" X Y X "> ] .~ = ( 0g ` J ) ) <-> ( J e. Mgm /\ [ <" X Y X "> ] ( .~ i^i ( A X. A ) ) = ( 0g ` J ) ) ) )
89 84 88 mpbird 
 |-  ( ph -> ( J e. Mgm /\ [ <" X Y X "> ] .~ = ( 0g ` J ) ) )