Metamath Proof Explorer

Theorem angmgmbas

Description: The base set of the angle addition magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses angmgmbas.p 
|- P = ( Base ` G )
angmgmbas.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmgmbas.c 
|- .~ = ( cgrA ` G )
angmgmbas.j 
|- J = ( AngMgm ` G )
angmgmbas.g 
|- ( ph -> G e. TarskiG )
Assertion angmgmbas 
|- ( ph -> ( A /. .~ ) = ( Base ` J ) )

Proof

Step Hyp Ref Expression
1 angmgmbas.p 
 |-  P = ( Base ` G )
2 angmgmbas.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmgmbas.c 
 |-  .~ = ( cgrA ` G )
4 angmgmbas.j 
 |-  J = ( AngMgm ` G )
5 angmgmbas.g 
 |-  ( ph -> G e. TarskiG )
6 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
7 eqid 
 |-  ( dist ` G ) = ( dist ` G )
8 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
9 eqid 
 |-  ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
10 eqid 
 |-  ( leA ` G ) = ( leA ` G )
11 1 2 6 7 3 8 9 4 10 angmgmval 
 |-  ( G e. TarskiG -> J = ( { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. } /s .~ ) )
12 5 11 syl 
 |-  ( ph -> J = ( { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. } /s .~ ) )
13 ovex 
 |-  ( P ^m ( 0 ..^ 3 ) ) e. _V
14 2 13 rabex2 
 |-  A e. _V
15 1nn 
 |-  1 e. NN
16 basendx 
 |-  ( Base ` ndx ) = 1
17 1lt2 
 |-  1 < 2
18 2nn 
 |-  2 e. NN
19 plusgndx 
 |-  ( +g ` ndx ) = 2
20 2lt10 
 |-  2 < ; 1 0
21 10nn 
 |-  ; 1 0 e. NN
22 plendx 
 |-  ( le ` ndx ) = ; 1 0
23 15 16 17 18 19 20 21 22 strle3 
 |-  { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. } Struct <. 1 , ; 1 0 >.
24 baseid 
 |-  Base = Slot ( Base ` ndx )
25 snsstp1 
 |-  { <. ( Base ` ndx ) , A >. } C_ { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. }
26 23 24 25 strfv 
 |-  ( A e. _V -> A = ( Base ` { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. } ) )
27 14 26 mp1i 
 |-  ( ph -> A = ( Base ` { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. } ) )
28 3 fvexi 
 |-  .~ e. _V
29 28 a1i 
 |-  ( ph -> .~ e. _V )
30 tpex 
 |-  { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. } e. _V
31 30 a1i 
 |-  ( ph -> { <. ( 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_ z e. P ( <" ( f ` 2 ) ( f ` 1 ) z "> .~ e /\ ( ( f ` 1 ) ( dist ` G ) z ) = ( ( e ` 1 ) ( dist ` G ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. P ( <" ( e ` 2 ) ( e ` 1 ) z "> .~ f /\ ( ( e ` 1 ) ( dist ` G ) z ) = ( ( f ` 1 ) ( dist ` G ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` G ) ( e ` 2 ) ) i^i ( z ( Itv ` G ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` G ) >. } e. _V )
32 12 27 29 31 qusbas 
 |-  ( ph -> ( A /. .~ ) = ( Base ` J ) )