Metamath Proof Explorer

Theorem angmgmval

Description: Explicit the value of the angle addition magma for a given geometry G . (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 )
angmgmval.s 
|- .<_ = ( leA ` G )
Assertion angmgmval 
|- ( G e. V -> J = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) )

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 angmgmval.s 
 |-  .<_ = ( leA ` G )
10 df-angmgm 
 |-  AngMgm = ( g e. _V |-> [_ ( Base ` g ) / p ]_ [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) )
11 fvexd 
 |-  ( g = G -> ( Base ` g ) e. _V )
12 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
13 12 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
14 eqid 
 |-  { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } = { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
15 ovexd 
 |-  ( ( g = G /\ p = P ) -> ( p ^m ( 0 ..^ 3 ) ) e. _V )
16 14 15 rabexd 
 |-  ( ( g = G /\ p = P ) -> { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } e. _V )
17 oveq1 
 |-  ( p = P -> ( p ^m ( 0 ..^ 3 ) ) = ( P ^m ( 0 ..^ 3 ) ) )
18 17 adantl 
 |-  ( ( g = G /\ p = P ) -> ( p ^m ( 0 ..^ 3 ) ) = ( P ^m ( 0 ..^ 3 ) ) )
19 18 rabeqdv 
 |-  ( ( g = G /\ p = P ) -> { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } )
20 19 2 eqtr4di 
 |-  ( ( g = G /\ p = P ) -> { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } = A )
21 opeq2 
 |-  ( a = A -> <. ( Base ` ndx ) , a >. = <. ( Base ` ndx ) , A >. )
22 21 adantl 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> <. ( Base ` ndx ) , a >. = <. ( Base ` ndx ) , A >. )
23 simpr 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> a = A )
24 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
25 24 ad2antrr 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( LineG ` g ) = ( LineG ` G ) )
26 25 6 eqtr4di 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( LineG ` g ) = L )
27 26 oveqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) = ( ( e ` 1 ) L ( e ` 2 ) ) )
28 27 eleq2d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) <-> ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) ) )
29 eqidd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( f ` 0 ) = ( f ` 0 ) )
30 eqidd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( f ` 1 ) = ( f ` 1 ) )
31 simplr 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> p = P )
32 fveq2 
 |-  ( g = G -> ( cgrA ` g ) = ( cgrA ` G ) )
33 32 5 eqtr4di 
 |-  ( g = G -> ( cgrA ` g ) = .~ )
34 33 ad2antrr 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( cgrA ` g ) = .~ )
35 34 breqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e <-> <" ( f ` 2 ) ( f ` 1 ) s "> .~ e ) )
36 fveq2 
 |-  ( g = G -> ( dist ` g ) = ( dist ` G ) )
37 36 4 eqtr4di 
 |-  ( g = G -> ( dist ` g ) = .- )
38 37 ad2antrr 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( dist ` g ) = .- )
39 38 oveqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( f ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) .- s ) )
40 38 oveqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) = ( ( e ` 1 ) .- ( e ` 0 ) ) )
41 39 40 eqeq12d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) <-> ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) )
42 35 41 anbi12d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) <-> ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) )
43 31 42 riotaeqbidv 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) = ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) )
44 29 30 43 s3eqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> = <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> )
45 eqidd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( e ` 0 ) = ( e ` 0 ) )
46 eqidd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( e ` 1 ) = ( e ` 1 ) )
47 34 breqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f <-> <" ( e ` 2 ) ( e ` 1 ) s "> .~ f ) )
48 38 oveqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( e ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) .- s ) )
49 38 oveqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) = ( ( f ` 1 ) .- ( f ` 0 ) ) )
50 48 49 eqeq12d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) <-> ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) ) )
51 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
52 51 3 eqtr4di 
 |-  ( g = G -> ( Itv ` g ) = I )
53 52 ad2antrr 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( Itv ` g ) = I )
54 53 oveqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( s ( Itv ` g ) ( e ` 0 ) ) = ( s I ( e ` 0 ) ) )
55 27 54 ineq12d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) = ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) )
56 55 neeq1d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) <-> ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) )
57 47 50 56 3anbi123d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) <-> ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) )
58 31 57 riotaeqbidv 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) = ( 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 ) ) ) =/= (/) ) ) )
59 45 46 58 s3eqd 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( 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 ) ) ) =/= (/) ) ) "> )
60 28 44 59 ifbieq12d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) = 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 ) ) ) =/= (/) ) ) "> ) )
61 23 23 60 mpoeq123dv 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) = ( 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 ) ) ) =/= (/) ) ) "> ) ) )
62 61 7 eqtr4di 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) = .+ )
63 62 opeq2d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. = <. ( +g ` ndx ) , .+ >. )
64 fveq2 
 |-  ( g = G -> ( leA ` g ) = ( leA ` G ) )
65 64 9 eqtr4di 
 |-  ( g = G -> ( leA ` g ) = .<_ )
66 65 opeq2d 
 |-  ( g = G -> <. ( le ` ndx ) , ( leA ` g ) >. = <. ( le ` ndx ) , .<_ >. )
67 66 ad2antrr 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> <. ( le ` ndx ) , ( leA ` g ) >. = <. ( le ` ndx ) , .<_ >. )
68 22 63 67 tpeq123d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } = { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } )
69 68 34 oveq12d 
 |-  ( ( ( g = G /\ p = P ) /\ a = A ) -> ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) )
70 16 20 69 csbied2 
 |-  ( ( g = G /\ p = P ) -> [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) )
71 11 13 70 csbied2 
 |-  ( g = G -> [_ ( Base ` g ) / p ]_ [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) )
72 elex 
 |-  ( G e. V -> G e. _V )
73 ovexd 
 |-  ( G e. V -> ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) e. _V )
74 10 71 72 73 fvmptd3 
 |-  ( G e. V -> ( AngMgm ` G ) = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) )
75 8 74 eqtrid 
 |-  ( G e. V -> J = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) )