Step |
Hyp |
Ref |
Expression |
1 |
|
tgsas.p |
|- P = ( Base ` G ) |
2 |
|
tgsas.m |
|- .- = ( dist ` G ) |
3 |
|
tgsas.i |
|- I = ( Itv ` G ) |
4 |
|
tgsas.g |
|- ( ph -> G e. TarskiG ) |
5 |
|
tgsas.a |
|- ( ph -> A e. P ) |
6 |
|
tgsas.b |
|- ( ph -> B e. P ) |
7 |
|
tgsas.c |
|- ( ph -> C e. P ) |
8 |
|
tgsas.d |
|- ( ph -> D e. P ) |
9 |
|
tgsas.e |
|- ( ph -> E e. P ) |
10 |
|
tgsas.f |
|- ( ph -> F e. P ) |
11 |
|
tgasa.l |
|- L = ( LineG ` G ) |
12 |
|
tgasa.1 |
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) ) |
13 |
|
tgasa.2 |
|- ( ph -> ( A .- B ) = ( D .- E ) ) |
14 |
|
tgasa.3 |
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> ) |
15 |
|
tgasa.4 |
|- ( ph -> <" C A B "> ( cgrA ` G ) <" F D E "> ) |
16 |
|
simprr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( E .- f ) = ( B .- C ) ) |
17 |
4
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> G e. TarskiG ) |
18 |
10
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> F e. P ) |
19 |
8
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> D e. P ) |
20 |
9
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> E e. P ) |
21 |
1 3 2 4 5 6 7 8 9 10 14 11 12
|
cgrancol |
|- ( ph -> -. ( F e. ( D L E ) \/ D = E ) ) |
22 |
21
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> -. ( F e. ( D L E ) \/ D = E ) ) |
23 |
|
eqid |
|- ( hlG ` G ) = ( hlG ` G ) |
24 |
|
simplr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f e. P ) |
25 |
7
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> C e. P ) |
26 |
5
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> A e. P ) |
27 |
6
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> B e. P ) |
28 |
12
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> -. ( C e. ( A L B ) \/ A = B ) ) |
29 |
4
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> G e. TarskiG ) |
30 |
8
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> D e. P ) |
31 |
9
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> E e. P ) |
32 |
10
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> F e. P ) |
33 |
5
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> A e. P ) |
34 |
6
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> B e. P ) |
35 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> C e. P ) |
36 |
1 3 4 23 5 6 7 8 9 10 14
|
cgracom |
|- ( ph -> <" D E F "> ( cgrA ` G ) <" A B C "> ) |
37 |
36
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> <" D E F "> ( cgrA ` G ) <" A B C "> ) |
38 |
|
simpr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> ( E e. ( D L F ) \/ D = F ) ) |
39 |
1 11 3 29 30 32 31 38
|
colcom |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> ( E e. ( F L D ) \/ F = D ) ) |
40 |
1 11 3 29 32 30 31 39
|
colrot1 |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> ( F e. ( D L E ) \/ D = E ) ) |
41 |
1 3 2 29 30 31 32 33 34 35 37 11 40
|
cgracol |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> ( C e. ( A L B ) \/ A = B ) ) |
42 |
12
|
ad3antrrr |
|- ( ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) /\ ( E e. ( D L F ) \/ D = F ) ) -> -. ( C e. ( A L B ) \/ A = B ) ) |
43 |
41 42
|
pm2.65da |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> -. ( E e. ( D L F ) \/ D = F ) ) |
44 |
|
eqid |
|- ( cgrG ` G ) = ( cgrG ` G ) |
45 |
14
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> ) |
46 |
|
simprl |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f ( ( hlG ` G ) ` E ) F ) |
47 |
1 3 23 17 26 27 25 19 20 18 45 24 46
|
cgrahl2 |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E f "> ) |
48 |
1 3 23 4 5 6 7 8 9 10 14
|
cgrane1 |
|- ( ph -> A =/= B ) |
49 |
1 3 23 5 5 6 4 48
|
hlid |
|- ( ph -> A ( ( hlG ` G ) ` B ) A ) |
50 |
49
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> A ( ( hlG ` G ) ` B ) A ) |
51 |
1 3 23 4 5 6 7 8 9 10 14
|
cgrane2 |
|- ( ph -> B =/= C ) |
52 |
51
|
necomd |
|- ( ph -> C =/= B ) |
53 |
1 3 23 7 5 6 4 52
|
hlid |
|- ( ph -> C ( ( hlG ` G ) ` B ) C ) |
54 |
53
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> C ( ( hlG ` G ) ` B ) C ) |
55 |
1 2 3 4 5 6 8 9 13
|
tgcgrcomlr |
|- ( ph -> ( B .- A ) = ( E .- D ) ) |
56 |
55
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( B .- A ) = ( E .- D ) ) |
57 |
16
|
eqcomd |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( B .- C ) = ( E .- f ) ) |
58 |
1 3 23 17 26 27 25 19 20 24 47 26 2 25 50 54 56 57
|
cgracgr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( A .- C ) = ( D .- f ) ) |
59 |
1 2 3 17 26 25 19 24 58
|
tgcgrcomlr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( C .- A ) = ( f .- D ) ) |
60 |
13
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( A .- B ) = ( D .- E ) ) |
61 |
1 2 44 17 25 26 27 24 19 20 59 60 57
|
trgcgr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> <" C A B "> ( cgrG ` G ) <" f D E "> ) |
62 |
1 3 11 4 7 5 6 12
|
ncolne1 |
|- ( ph -> C =/= A ) |
63 |
62
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> C =/= A ) |
64 |
1 2 3 17 25 26 24 19 59 63
|
tgcgrneq |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f =/= D ) |
65 |
1 3 23 24 18 19 17 64
|
hlid |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f ( ( hlG ` G ) ` D ) f ) |
66 |
1 3 23 4 7 5 6 10 8 9 15
|
cgrane4 |
|- ( ph -> D =/= E ) |
67 |
66
|
necomd |
|- ( ph -> E =/= D ) |
68 |
1 3 23 9 5 8 4 67
|
hlid |
|- ( ph -> E ( ( hlG ` G ) ` D ) E ) |
69 |
68
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> E ( ( hlG ` G ) ` D ) E ) |
70 |
1 3 23 17 25 26 27 24 19 20 24 20 61 65 69
|
iscgrad |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> <" C A B "> ( cgrA ` G ) <" f D E "> ) |
71 |
66
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> D =/= E ) |
72 |
1 3 17 23 24 19 20 64 71
|
cgraswap |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> <" f D E "> ( cgrA ` G ) <" E D f "> ) |
73 |
1 3 17 23 25 26 27 24 19 20 70 20 19 24 72
|
cgratr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> <" C A B "> ( cgrA ` G ) <" E D f "> ) |
74 |
1 3 23 4 7 5 6 10 8 9 15
|
cgrane3 |
|- ( ph -> D =/= F ) |
75 |
74
|
necomd |
|- ( ph -> F =/= D ) |
76 |
1 3 4 23 10 8 9 75 66
|
cgraswap |
|- ( ph -> <" F D E "> ( cgrA ` G ) <" E D F "> ) |
77 |
1 3 4 23 7 5 6 10 8 9 15 9 8 10 76
|
cgratr |
|- ( ph -> <" C A B "> ( cgrA ` G ) <" E D F "> ) |
78 |
77
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> <" C A B "> ( cgrA ` G ) <" E D F "> ) |
79 |
1 3 11 4 9 8 67
|
tgelrnln |
|- ( ph -> ( E L D ) e. ran L ) |
80 |
79
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( E L D ) e. ran L ) |
81 |
|
simpl |
|- ( ( a = u /\ b = v ) -> a = u ) |
82 |
81
|
eleq1d |
|- ( ( a = u /\ b = v ) -> ( a e. ( P \ ( E L D ) ) <-> u e. ( P \ ( E L D ) ) ) ) |
83 |
|
simpr |
|- ( ( a = u /\ b = v ) -> b = v ) |
84 |
83
|
eleq1d |
|- ( ( a = u /\ b = v ) -> ( b e. ( P \ ( E L D ) ) <-> v e. ( P \ ( E L D ) ) ) ) |
85 |
82 84
|
anbi12d |
|- ( ( a = u /\ b = v ) -> ( ( a e. ( P \ ( E L D ) ) /\ b e. ( P \ ( E L D ) ) ) <-> ( u e. ( P \ ( E L D ) ) /\ v e. ( P \ ( E L D ) ) ) ) ) |
86 |
|
simpr |
|- ( ( ( a = u /\ b = v ) /\ t = w ) -> t = w ) |
87 |
|
simpll |
|- ( ( ( a = u /\ b = v ) /\ t = w ) -> a = u ) |
88 |
|
simplr |
|- ( ( ( a = u /\ b = v ) /\ t = w ) -> b = v ) |
89 |
87 88
|
oveq12d |
|- ( ( ( a = u /\ b = v ) /\ t = w ) -> ( a I b ) = ( u I v ) ) |
90 |
86 89
|
eleq12d |
|- ( ( ( a = u /\ b = v ) /\ t = w ) -> ( t e. ( a I b ) <-> w e. ( u I v ) ) ) |
91 |
90
|
cbvrexdva |
|- ( ( a = u /\ b = v ) -> ( E. t e. ( E L D ) t e. ( a I b ) <-> E. w e. ( E L D ) w e. ( u I v ) ) ) |
92 |
85 91
|
anbi12d |
|- ( ( a = u /\ b = v ) -> ( ( ( a e. ( P \ ( E L D ) ) /\ b e. ( P \ ( E L D ) ) ) /\ E. t e. ( E L D ) t e. ( a I b ) ) <-> ( ( u e. ( P \ ( E L D ) ) /\ v e. ( P \ ( E L D ) ) ) /\ E. w e. ( E L D ) w e. ( u I v ) ) ) ) |
93 |
92
|
cbvopabv |
|- { <. a , b >. | ( ( a e. ( P \ ( E L D ) ) /\ b e. ( P \ ( E L D ) ) ) /\ E. t e. ( E L D ) t e. ( a I b ) ) } = { <. u , v >. | ( ( u e. ( P \ ( E L D ) ) /\ v e. ( P \ ( E L D ) ) ) /\ E. w e. ( E L D ) w e. ( u I v ) ) } |
94 |
1 3 11 4 9 8 67
|
tglinerflx1 |
|- ( ph -> E e. ( E L D ) ) |
95 |
94
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> E e. ( E L D ) ) |
96 |
1 11 3 4 8 9 10 21
|
ncolcom |
|- ( ph -> -. ( F e. ( E L D ) \/ E = D ) ) |
97 |
|
pm2.45 |
|- ( -. ( F e. ( E L D ) \/ E = D ) -> -. F e. ( E L D ) ) |
98 |
96 97
|
syl |
|- ( ph -> -. F e. ( E L D ) ) |
99 |
98
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> -. F e. ( E L D ) ) |
100 |
1 3 23 24 18 20 17 46
|
hlcomd |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> F ( ( hlG ` G ) ` E ) f ) |
101 |
1 3 11 17 80 20 93 23 95 18 24 99 100
|
hphl |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> F ( ( hpG ` G ) ` ( E L D ) ) f ) |
102 |
1 3 11 17 80 18 93 24 101
|
hpgcom |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f ( ( hpG ` G ) ` ( E L D ) ) F ) |
103 |
1 3 11 4 79 10 93 98
|
hpgid |
|- ( ph -> F ( ( hpG ` G ) ` ( E L D ) ) F ) |
104 |
103
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> F ( ( hpG ` G ) ` ( E L D ) ) F ) |
105 |
1 3 2 17 25 26 27 20 19 18 11 28 43 24 18 23 73 78 102 104
|
acopyeu |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f ( ( hlG ` G ) ` D ) F ) |
106 |
1 3 23 24 18 19 17 11 105
|
hlln |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f e. ( F L D ) ) |
107 |
1 3 11 4 10 8 75
|
tglinerflx1 |
|- ( ph -> F e. ( F L D ) ) |
108 |
107
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> F e. ( F L D ) ) |
109 |
1 3 23 4 5 6 7 8 9 10 14
|
cgrane4 |
|- ( ph -> E =/= F ) |
110 |
109
|
ad2antrr |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> E =/= F ) |
111 |
1 3 23 24 18 20 17 11 46
|
hlln |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f e. ( F L E ) ) |
112 |
1 3 11 17 20 18 24 110 111
|
lncom |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f e. ( E L F ) ) |
113 |
1 3 11 17 20 18 110
|
tglinerflx2 |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> F e. ( E L F ) ) |
114 |
1 3 11 17 18 19 20 18 22 106 108 112 113
|
tglineinteq |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> f = F ) |
115 |
114
|
oveq2d |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( E .- f ) = ( E .- F ) ) |
116 |
16 115
|
eqtr3d |
|- ( ( ( ph /\ f e. P ) /\ ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) -> ( B .- C ) = ( E .- F ) ) |
117 |
109
|
necomd |
|- ( ph -> F =/= E ) |
118 |
1 3 23 9 6 7 4 10 2 117 51
|
hlcgrex |
|- ( ph -> E. f e. P ( f ( ( hlG ` G ) ` E ) F /\ ( E .- f ) = ( B .- C ) ) ) |
119 |
116 118
|
r19.29a |
|- ( ph -> ( B .- C ) = ( E .- F ) ) |