Metamath Proof Explorer

Theorem angmgmaddlid

Description: The left identity element for the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses angmgmadd.p 
|- P = ( Base ` G )
angmgmadd.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmgmadd.i 
|- I = ( Itv ` G )
angmgmadd.d 
|- .- = ( dist ` G )
angmgmadd.c 
|- .~ = ( cgrA ` G )
angmgmadd.l 
|- L = ( LineG ` G )
angmgmadd.g 
|- ( ph -> G e. TarskiG )
angmgmadd.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 ) ) ) =/= (/) ) ) "> ) )
angmgmaddlid.x 
|- ( ph -> X e. P )
angmgmaddlid.y 
|- ( ph -> Y e. ( P \ { X } ) )
angmgmaddlid.e 
|- ( ph -> E e. A )
Assertion angmgmaddlid 
|- ( ph -> ( <" X Y X "> .+ E ) .~ E )

Proof

Step Hyp Ref Expression
1 angmgmadd.p 
 |-  P = ( Base ` G )
2 angmgmadd.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmgmadd.i 
 |-  I = ( Itv ` G )
4 angmgmadd.d 
 |-  .- = ( dist ` G )
5 angmgmadd.c 
 |-  .~ = ( cgrA ` G )
6 angmgmadd.l 
 |-  L = ( LineG ` G )
7 angmgmadd.g 
 |-  ( ph -> G e. TarskiG )
8 angmgmadd.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 ) ) ) =/= (/) ) ) "> ) )
9 angmgmaddlid.x 
 |-  ( ph -> X e. P )
10 angmgmaddlid.y 
 |-  ( ph -> Y e. ( P \ { X } ) )
11 angmgmaddlid.e 
 |-  ( ph -> E e. A )
12 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> E = <" u v w "> )
13 12 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( <" X Y X "> .+ E ) = ( <" X Y X "> .+ <" u v w "> ) )
14 7 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> G e. TarskiG )
15 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> u e. P )
16 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> v e. P )
17 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> w e. P )
18 9 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> X e. P )
19 10 eldifad 
 |-  ( ph -> Y e. P )
20 19 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> Y e. P )
21 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> u =/= v )
22 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> v =/= w )
23 10 eldifsnbd 
 |-  ( ph -> Y =/= X )
24 23 necomd 
 |-  ( ph -> X =/= Y )
25 24 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> X =/= Y )
26 25 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> Y =/= X )
27 1 3 6 14 20 18 26 tglinerflx2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> X e. ( Y L X ) )
28 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t e. P )
29 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
30 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t ( ( hlG ` G ) ` v ) w )
31 1 3 29 28 17 16 14 30 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> w ( ( hlG ` G ) ` v ) t )
32 1 3 29 18 15 20 14 25 hlid 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> X ( ( hlG ` G ) ` Y ) X )
33 1 5 29 14 31 32 16 20 zerocgra 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" w v t "> .~ <" X Y X "> )
34 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( v .- t ) = ( Y .- X ) )
35 1 2 3 4 5 6 14 15 16 17 18 20 18 21 22 25 26 8 27 28 33 34 angmgmaddov2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( <" X Y X "> .+ <" u v w "> ) = <" u v t "> )
36 13 35 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( <" X Y X "> .+ E ) = <" u v t "> )
37 5 eqcomi 
 |-  ( cgrA ` G ) = .~
38 37 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( cgrA ` G ) = .~ )
39 34 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( Y .- X ) = ( v .- t ) )
40 1 4 3 14 20 18 16 28 39 26 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> v =/= t )
41 1 3 14 29 15 16 28 21 40 cgraid 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" u v t "> ( cgrA ` G ) <" u v t "> )
42 1 3 29 14 15 16 28 15 16 28 41 17 31 cgrahl2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" u v t "> ( cgrA ` G ) <" u v w "> )
43 38 42 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" u v t "> .~ <" u v w "> )
44 36 43 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( <" X Y X "> .+ E ) .~ <" u v w "> )
45 44 anasss 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ t e. P ) /\ ( t ( ( hlG ` G ) ` v ) w /\ ( v .- t ) = ( Y .- X ) ) ) -> ( <" X Y X "> .+ E ) .~ <" u v w "> )
46 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> v e. P )
47 19 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> Y e. P )
48 9 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> X e. P )
49 7 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> G e. TarskiG )
50 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> w e. P )
51 simpr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> v =/= w )
52 51 necomd 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> w =/= v )
53 23 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> Y =/= X )
54 1 3 29 46 47 48 49 50 4 52 53 hlcgrex 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> E. t e. P ( t ( ( hlG ` G ) ` v ) w /\ ( v .- t ) = ( Y .- X ) ) )
55 45 54 r19.29a 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> ( <" X Y X "> .+ E ) .~ <" u v w "> )
56 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> E = <" u v w "> )
57 55 56 breqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> ( <" X Y X "> .+ E ) .~ E )
58 57 anasss 
 |-  ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ ( u =/= v /\ v =/= w ) ) -> ( <" X Y X "> .+ E ) .~ E )
59 58 anasss 
 |-  ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ ( E = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> ( <" X Y X "> .+ E ) .~ E )
60 59 r19.29an 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ E. w e. P ( E = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> ( <" X Y X "> .+ E ) .~ E )
61 1 fvexi 
 |-  P e. _V
62 61 2 11 elcgrabasi 
 |-  ( ph -> E. u e. P E. v e. P E. w e. P ( E = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) )
63 60 62 r19.29vva 
 |-  ( ph -> ( <" X Y X "> .+ E ) .~ E )