Metamath Proof Explorer

Theorem tgasa1

Description: Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of Schwabhauser p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Hypotheses tgsas.p 
|- P = ( Base ` G )
tgsas.m 
|- .- = ( dist ` G )
tgsas.i 
|- I = ( Itv ` G )
tgsas.g 
|- ( ph -> G e. TarskiG )
tgsas.a 
|- ( ph -> A e. P )
tgsas.b 
|- ( ph -> B e. P )
tgsas.c 
|- ( ph -> C e. P )
tgsas.d 
|- ( ph -> D e. P )
tgsas.e 
|- ( ph -> E e. P )
tgsas.f 
|- ( ph -> F e. P )
tgasa.l 
|- L = ( LineG ` G )
tgasa.1 
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
tgasa.2 
|- ( ph -> ( A .- B ) = ( D .- E ) )
tgasa.3 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
tgasa.4 
|- ( ph -> <" C A B "> ( cgrA ` G ) <" F D E "> )
Assertion tgasa1 
|- ( ph -> ( B .- C ) = ( E .- F ) )

Proof

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 ) )