Metamath Proof Explorer

Theorem angmgm0g

Description: The identity element of the angle addition magma. (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 angmgm0g 
|- ( ph -> [ <" 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 1 2 3 4 5 6 7 8 9 10 11 angmgmlem 
 |-  ( ph -> ( J e. Mgm /\ [ <" X Y X "> ] .~ = ( 0g ` J ) ) )
13 12 simprd 
 |-  ( ph -> [ <" X Y X "> ] .~ = ( 0g ` J ) )