Metamath Proof Explorer

Theorem angmgmaddrid

Description: The right 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 angmgmaddrid 
|- ( ph -> ( E .+ <" X Y X "> ) .~ 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-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> E = <" u v w "> )
13 12 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> ( E .+ <" X Y X "> ) = ( <" u v w "> .+ <" X Y X "> ) )
14 7 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> G e. TarskiG )
15 14 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> G e. TarskiG )
16 9 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> X e. P )
17 16 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> X e. P )
18 10 eldifad 
 |-  ( ph -> Y e. P )
19 18 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> Y e. P )
20 19 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> Y e. P )
21 simp-7r 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> u e. P )
22 21 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> u e. P )
23 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> v e. P )
24 23 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> v e. P )
25 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> w e. P )
26 25 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> w e. P )
27 10 eldifsnbd 
 |-  ( ph -> Y =/= X )
28 27 necomd 
 |-  ( ph -> X =/= Y )
29 28 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> X =/= Y )
30 29 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> X =/= Y )
31 27 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> Y =/= X )
32 31 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> Y =/= X )
33 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> u =/= v )
34 33 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> u =/= v )
35 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> v =/= w )
36 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> u e. ( v L w ) )
37 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> t e. P )
38 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
39 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> t ( ( hlG ` G ) ` Y ) X )
40 1 3 38 37 17 20 15 39 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> X ( ( hlG ` G ) ` Y ) t )
41 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> w ( ( hlG ` G ) ` v ) u )
42 1 3 38 26 22 24 15 41 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> u ( ( hlG ` G ) ` v ) w )
43 1 5 38 15 40 42 20 24 zerocgra 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> <" X Y t "> .~ <" u v w "> )
44 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> ( Y .- t ) = ( v .- u ) )
45 1 2 3 4 5 6 15 17 20 17 22 24 26 30 32 34 35 8 36 37 43 44 angmgmaddov2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> ( <" u v w "> .+ <" X Y X "> ) = <" X Y t "> )
46 13 45 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> ( E .+ <" X Y X "> ) = <" X Y t "> )
47 46 43 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ t ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- t ) = ( v .- u ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
48 47 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Y ) X /\ ( Y .- t ) = ( v .- u ) ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
49 18 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> Y e. P )
50 23 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> v e. P )
51 21 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> u e. P )
52 14 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> G e. TarskiG )
53 16 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> X e. P )
54 28 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> X =/= Y )
55 33 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> u =/= v )
56 55 necomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> v =/= u )
57 1 3 38 49 50 51 52 53 4 54 56 hlcgrex 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> E. t e. P ( t ( ( hlG ` G ) ` Y ) X /\ ( Y .- t ) = ( v .- u ) ) )
58 48 57 r19.29a 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ w ( ( hlG ` G ) ` v ) u ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
59 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> E = <" u v w "> )
60 59 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> ( E .+ <" X Y X "> ) = ( <" u v w "> .+ <" X Y X "> ) )
61 14 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) -> G e. TarskiG )
62 61 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> G e. TarskiG )
63 16 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) -> X e. P )
64 63 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> X e. P )
65 18 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) -> Y e. P )
66 65 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> Y e. P )
67 21 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) -> u e. P )
68 67 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> u e. P )
69 23 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) -> v e. P )
70 69 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> v e. P )
71 25 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> w e. P )
72 29 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> X =/= Y )
73 72 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> Y =/= X )
74 33 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> u =/= v )
75 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> v =/= w )
76 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> u e. ( v L w ) )
77 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> t e. P )
78 5 eqcomi 
 |-  ( cgrA ` G ) = .~
79 78 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> ( cgrA ` G ) = .~ )
80 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> Y e. ( X I t ) )
81 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> v e. ( u I w ) )
82 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> ( Y .- t ) = ( v .- u ) )
83 82 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> ( v .- u ) = ( Y .- t ) )
84 74 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> v =/= u )
85 1 4 3 62 70 68 66 77 83 84 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> Y =/= t )
86 85 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> t =/= Y )
87 75 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> w =/= v )
88 1 3 4 62 64 66 77 68 70 71 80 81 72 86 74 87 flatcgra 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> <" X Y t "> ( cgrA ` G ) <" u v w "> )
89 79 88 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> <" X Y t "> .~ <" u v w "> )
90 1 2 3 4 5 6 62 64 66 64 68 70 71 72 73 74 75 8 76 77 89 82 angmgmaddov2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> ( <" u v w "> .+ <" X Y X "> ) = <" X Y t "> )
91 60 90 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> ( E .+ <" X Y X "> ) = <" X Y t "> )
92 91 89 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ Y e. ( X I t ) ) /\ ( Y .- t ) = ( v .- u ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
93 92 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) /\ t e. P ) /\ ( Y e. ( X I t ) /\ ( Y .- t ) = ( v .- u ) ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
94 1 4 3 61 63 65 69 67 axtgsegcon 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) -> E. t e. P ( Y e. ( X I t ) /\ ( Y .- t ) = ( v .- u ) ) )
95 93 94 r19.29a 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) /\ v e. ( u I w ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
96 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> u e. ( v L w ) )
97 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> v =/= w )
98 1 3 6 14 21 23 25 33 96 97 lnrot2 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> w e. ( u L v ) )
99 1 3 38 21 23 25 14 16 6 98 lnhl 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> ( w ( ( hlG ` G ) ` v ) u \/ v e. ( u I w ) ) )
100 58 95 99 mpjaodan 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ u e. ( v L w ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
101 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> E = <" u v w "> )
102 101 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( E .+ <" X Y X "> ) = ( <" u v w "> .+ <" X Y X "> ) )
103 7 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> G e. TarskiG )
104 103 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> G e. TarskiG )
105 9 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> X e. P )
106 105 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> X e. P )
107 18 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> Y e. P )
108 107 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> Y e. P )
109 simp-10r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> u e. P )
110 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> v e. P )
111 110 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> v e. P )
112 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> w e. P )
113 112 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> w e. P )
114 28 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> X =/= Y )
115 27 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> Y =/= X )
116 115 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> Y =/= X )
117 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> u =/= v )
118 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> v =/= w )
119 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> -. u e. ( v L w ) )
120 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t e. P )
121 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t ( ( hlG ` G ) ` v ) w )
122 1 3 38 120 113 111 104 121 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> w ( ( hlG ` G ) ` v ) t )
123 1 3 38 106 106 108 104 114 hlid 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> X ( ( hlG ` G ) ` Y ) X )
124 1 5 38 104 122 123 111 108 zerocgra 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" w v t "> .~ <" X Y X "> )
125 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( v .- t ) = ( Y .- X ) )
126 1 3 38 113 120 111 104 6 122 hlln 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> w e. ( t L v ) )
127 1 6 3 104 120 111 126 tglngne 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t =/= v )
128 1 3 6 104 111 113 120 118 126 127 lnrot1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t e. ( v L w ) )
129 1 4 3 104 120 109 tgbtwntriv1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t e. ( t I u ) )
130 128 129 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> t e. ( ( v L w ) i^i ( t I u ) ) )
131 130 ne0d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( ( v L w ) i^i ( t I u ) ) =/= (/) )
132 1 2 3 4 5 6 104 106 108 106 109 111 113 114 116 117 118 8 119 120 124 125 131 angmgmaddov1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( <" u v w "> .+ <" X Y X "> ) = <" u v t "> )
133 102 132 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( E .+ <" X Y X "> ) = <" u v t "> )
134 78 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( cgrA ` G ) = .~ )
135 127 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> v =/= t )
136 1 3 104 38 109 111 120 117 135 cgraid 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" u v t "> ( cgrA ` G ) <" u v t "> )
137 1 3 38 104 109 111 120 109 111 120 136 113 122 cgrahl2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" u v t "> ( cgrA ` G ) <" u v w "> )
138 134 137 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> <" u v t "> .~ <" u v w "> )
139 133 138 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ t ( ( hlG ` G ) ` v ) w ) /\ ( v .- t ) = ( Y .- X ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
140 139 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) /\ t e. P ) /\ ( t ( ( hlG ` G ) ` v ) w /\ ( v .- t ) = ( Y .- X ) ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
141 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> v =/= w )
142 141 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> w =/= v )
143 1 3 38 110 107 105 103 112 4 142 115 hlcgrex 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> E. t e. P ( t ( ( hlG ` G ) ` v ) w /\ ( v .- t ) = ( Y .- X ) ) )
144 140 143 r19.29a 
 |-  ( ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ -. u e. ( v L w ) ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
145 100 144 pm2.61dan 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> ( E .+ <" X Y X "> ) .~ <" u v w "> )
146 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> E = <" u v w "> )
147 145 146 breqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> ( E .+ <" X Y X "> ) .~ E )
148 147 anasss 
 |-  ( ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ E = <" u v w "> ) /\ ( u =/= v /\ v =/= w ) ) -> ( E .+ <" X Y X "> ) .~ E )
149 148 anasss 
 |-  ( ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ ( E = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> ( E .+ <" X Y X "> ) .~ E )
150 149 r19.29an 
 |-  ( ( ( ( ph /\ u e. P ) /\ v e. P ) /\ E. w e. P ( E = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> ( E .+ <" X Y X "> ) .~ E )
151 1 fvexi 
 |-  P e. _V
152 151 2 11 elcgrabasi 
 |-  ( ph -> E. u e. P E. v e. P E. w e. P ( E = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) )
153 150 152 r19.29vva 
 |-  ( ph -> ( E .+ <" X Y X "> ) .~ E )