Metamath Proof Explorer

Theorem hypcgrlem1

Description: Lemma for hypcgr , case where triangles share a cathetus. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses hypcgr.p 
|- P = ( Base ` G )
hypcgr.m 
|- .- = ( dist ` G )
hypcgr.i 
|- I = ( Itv ` G )
hypcgr.g 
|- ( ph -> G e. TarskiG )
hypcgr.h 
|- ( ph -> G TarskiGDim>= 2 )
hypcgr.a 
|- ( ph -> A e. P )
hypcgr.b 
|- ( ph -> B e. P )
hypcgr.c 
|- ( ph -> C e. P )
hypcgr.d 
|- ( ph -> D e. P )
hypcgr.e 
|- ( ph -> E e. P )
hypcgr.f 
|- ( ph -> F e. P )
hypcgr.1 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
hypcgr.2 
|- ( ph -> <" D E F "> e. ( raG ` G ) )
hypcgr.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
hypcgr.4 
|- ( ph -> ( B .- C ) = ( E .- F ) )
hypcgrlem2.b 
|- ( ph -> B = E )
hypcgrlem1.s 
|- S = ( ( lInvG ` G ) ` ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) )
hypcgrlem1.a 
|- ( ph -> C = F )
Assertion hypcgrlem1 
|- ( ph -> ( A .- C ) = ( D .- F ) )

Proof

Step Hyp Ref Expression
1 hypcgr.p 
 |-  P = ( Base ` G )
2 hypcgr.m 
 |-  .- = ( dist ` G )
3 hypcgr.i 
 |-  I = ( Itv ` G )
4 hypcgr.g 
 |-  ( ph -> G e. TarskiG )
5 hypcgr.h 
 |-  ( ph -> G TarskiGDim>= 2 )
6 hypcgr.a 
 |-  ( ph -> A e. P )
7 hypcgr.b 
 |-  ( ph -> B e. P )
8 hypcgr.c 
 |-  ( ph -> C e. P )
9 hypcgr.d 
 |-  ( ph -> D e. P )
10 hypcgr.e 
 |-  ( ph -> E e. P )
11 hypcgr.f 
 |-  ( ph -> F e. P )
12 hypcgr.1 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
13 hypcgr.2 
 |-  ( ph -> <" D E F "> e. ( raG ` G ) )
14 hypcgr.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
15 hypcgr.4 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )
16 hypcgrlem2.b 
 |-  ( ph -> B = E )
17 hypcgrlem1.s 
 |-  S = ( ( lInvG ` G ) ` ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) )
18 hypcgrlem1.a 
 |-  ( ph -> C = F )
19 4 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> G e. TarskiG )
20 8 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> C e. P )
21 6 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> A e. P )
22 11 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> F e. P )
23 9 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> D e. P )
24 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
25 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
26 1 2 3 24 25 4 6 7 8 12 ragcom 
 |-  ( ph -> <" C B A "> e. ( raG ` G ) )
27 1 2 3 24 25 4 8 7 6 israg 
 |-  ( ph -> ( <" C B A "> e. ( raG ` G ) <-> ( C .- A ) = ( C .- ( ( ( pInvG ` G ) ` B ) ` A ) ) ) )
28 26 27 mpbid 
 |-  ( ph -> ( C .- A ) = ( C .- ( ( ( pInvG ` G ) ` B ) ` A ) ) )
29 28 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> ( C .- A ) = ( C .- ( ( ( pInvG ` G ) ` B ) ` A ) ) )
30 18 eqcomd 
 |-  ( ph -> F = C )
31 30 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> F = C )
32 1 2 3 4 5 6 9 25 7 ismidb 
 |-  ( ph -> ( D = ( ( ( pInvG ` G ) ` B ) ` A ) <-> ( A ( midG ` G ) D ) = B ) )
33 32 biimpar 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> D = ( ( ( pInvG ` G ) ` B ) ` A ) )
34 31 33 oveq12d 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> ( F .- D ) = ( C .- ( ( ( pInvG ` G ) ` B ) ` A ) ) )
35 29 34 eqtr4d 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> ( C .- A ) = ( F .- D ) )
36 1 2 3 19 20 21 22 23 35 tgcgrcomlr 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) = B ) -> ( A .- C ) = ( D .- F ) )
37 simpr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = D ) -> A = D )
38 18 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = D ) -> C = F )
39 37 38 oveq12d 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = D ) -> ( A .- C ) = ( D .- F ) )
40 12 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> <" A B C "> e. ( raG ` G ) )
41 4 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> G e. TarskiG )
42 6 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> A e. P )
43 7 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> B e. P )
44 8 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> C e. P )
45 1 2 3 24 25 41 42 43 44 israg 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( ( pInvG ` G ) ` B ) ` C ) ) ) )
46 40 45 mpbid 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A .- C ) = ( A .- ( ( ( pInvG ` G ) ` B ) ` C ) ) )
47 5 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> G TarskiGDim>= 2 )
48 9 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> D e. P )
49 1 2 3 41 47 42 48 midcl 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) e. P )
50 simplr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) =/= B )
51 1 3 24 41 49 43 50 tgelrnln 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) e. ran ( LineG ` G ) )
52 eqid 
 |-  ( ( pInvG ` G ) ` B ) = ( ( pInvG ` G ) ` B )
53 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
54 1 2 3 24 25 41 43 52 44 mircl 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( ( ( pInvG ` G ) ` B ) ` C ) e. P )
55 simpr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> A =/= D )
56 1 2 3 41 47 42 48 midbtwn 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) e. ( A I D ) )
57 1 24 3 41 42 49 48 56 btwncolg3 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( D e. ( A ( LineG ` G ) ( A ( midG ` G ) D ) ) \/ A = ( A ( midG ` G ) D ) ) )
58 eqidd 
 |-  ( ph -> D = D )
59 58 16 18 s3eqd 
 |-  ( ph -> <" D B C "> = <" D E F "> )
60 59 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> <" D B C "> = <" D E F "> )
61 13 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> <" D E F "> e. ( raG ` G ) )
62 60 61 eqeltrd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> <" D B C "> e. ( raG ` G ) )
63 1 2 3 24 25 41 48 43 44 israg 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( <" D B C "> e. ( raG ` G ) <-> ( D .- C ) = ( D .- ( ( ( pInvG ` G ) ` B ) ` C ) ) ) )
64 62 63 mpbid 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( D .- C ) = ( D .- ( ( ( pInvG ` G ) ` B ) ` C ) ) )
65 1 24 3 41 42 48 49 53 44 54 2 55 57 46 64 lncgr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( ( A ( midG ` G ) D ) .- C ) = ( ( A ( midG ` G ) D ) .- ( ( ( pInvG ` G ) ` B ) ` C ) ) )
66 1 2 3 24 25 41 49 43 44 israg 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( <" ( A ( midG ` G ) D ) B C "> e. ( raG ` G ) <-> ( ( A ( midG ` G ) D ) .- C ) = ( ( A ( midG ` G ) D ) .- ( ( ( pInvG ` G ) ` B ) ` C ) ) ) )
67 65 66 mpbird 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> <" ( A ( midG ` G ) D ) B C "> e. ( raG ` G ) )
68 1 3 24 41 49 43 50 tglinerflx1 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) e. ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) )
69 1 3 24 41 49 43 50 tglinerflx2 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> B e. ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) )
70 1 2 3 41 47 17 24 51 49 52 67 68 69 44 50 lmimid 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( S ` C ) = ( ( ( pInvG ` G ) ` B ) ` C ) )
71 70 oveq2d 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A .- ( S ` C ) ) = ( A .- ( ( ( pInvG ` G ) ` B ) ` C ) ) )
72 46 71 eqtr4d 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A .- C ) = ( A .- ( S ` C ) ) )
73 1 2 3 41 47 48 42 midcom 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( D ( midG ` G ) A ) = ( A ( midG ` G ) D ) )
74 73 68 eqeltrd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( D ( midG ` G ) A ) e. ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) )
75 55 necomd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> D =/= A )
76 1 3 24 41 48 42 75 tgelrnln 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( D ( LineG ` G ) A ) e. ran ( LineG ` G ) )
77 1 2 3 41 42 49 48 56 tgbtwncom 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) e. ( D I A ) )
78 1 3 24 41 48 42 49 75 77 btwnlng1 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) e. ( D ( LineG ` G ) A ) )
79 68 78 elind 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) e. ( ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) i^i ( D ( LineG ` G ) A ) ) )
80 1 3 24 41 48 42 75 tglinerflx2 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> A e. ( D ( LineG ` G ) A ) )
81 50 necomd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> B =/= ( A ( midG ` G ) D ) )
82 4 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> G e. TarskiG )
83 6 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> A e. P )
84 9 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> D e. P )
85 5 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> G TarskiGDim>= 2 )
86 simpr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> A = ( A ( midG ` G ) D ) )
87 86 eqcomd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> ( A ( midG ` G ) D ) = A )
88 1 2 3 82 85 83 84 87 midcgr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> ( A .- A ) = ( A .- D ) )
89 88 eqcomd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> ( A .- D ) = ( A .- A ) )
90 1 2 3 82 83 84 83 89 axtgcgrid 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A = ( A ( midG ` G ) D ) ) -> A = D )
91 90 ex 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) -> ( A = ( A ( midG ` G ) D ) -> A = D ) )
92 91 necon3d 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) -> ( A =/= D -> A =/= ( A ( midG ` G ) D ) ) )
93 92 imp 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> A =/= ( A ( midG ` G ) D ) )
94 1 2 3 4 6 7 9 10 14 tgcgrcomlr 
 |-  ( ph -> ( B .- A ) = ( E .- D ) )
95 16 oveq1d 
 |-  ( ph -> ( B .- D ) = ( E .- D ) )
96 94 95 eqtr4d 
 |-  ( ph -> ( B .- A ) = ( B .- D ) )
97 96 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( B .- A ) = ( B .- D ) )
98 eqidd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A ( midG ` G ) D ) = ( A ( midG ` G ) D ) )
99 1 2 3 41 47 42 48 25 49 ismidb 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( D = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) D ) ) ` A ) <-> ( A ( midG ` G ) D ) = ( A ( midG ` G ) D ) ) )
100 98 99 mpbird 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> D = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) D ) ) ` A ) )
101 100 oveq2d 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( B .- D ) = ( B .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) D ) ) ` A ) ) )
102 97 101 eqtrd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( B .- A ) = ( B .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) D ) ) ` A ) ) )
103 1 2 3 24 25 41 43 49 42 israg 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( <" B ( A ( midG ` G ) D ) A "> e. ( raG ` G ) <-> ( B .- A ) = ( B .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) D ) ) ` A ) ) ) )
104 102 103 mpbird 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> <" B ( A ( midG ` G ) D ) A "> e. ( raG ` G ) )
105 1 2 3 24 41 51 76 79 69 80 81 93 104 ragperp 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) ( perpG ` G ) ( D ( LineG ` G ) A ) )
106 105 orcd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) ( perpG ` G ) ( D ( LineG ` G ) A ) \/ D = A ) )
107 1 2 3 41 47 17 24 51 48 42 islmib 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A = ( S ` D ) <-> ( ( D ( midG ` G ) A ) e. ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) /\ ( ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) ( perpG ` G ) ( D ( LineG ` G ) A ) \/ D = A ) ) ) )
108 74 106 107 mpbir2and 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> A = ( S ` D ) )
109 108 oveq1d 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A .- ( S ` C ) ) = ( ( S ` D ) .- ( S ` C ) ) )
110 1 2 3 41 47 17 24 51 48 44 lmiiso 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( ( S ` D ) .- ( S ` C ) ) = ( D .- C ) )
111 18 oveq2d 
 |-  ( ph -> ( D .- C ) = ( D .- F ) )
112 111 ad2antrr 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( D .- C ) = ( D .- F ) )
113 109 110 112 3eqtrd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A .- ( S ` C ) ) = ( D .- F ) )
114 72 113 eqtrd 
 |-  ( ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) /\ A =/= D ) -> ( A .- C ) = ( D .- F ) )
115 39 114 pm2.61dane 
 |-  ( ( ph /\ ( A ( midG ` G ) D ) =/= B ) -> ( A .- C ) = ( D .- F ) )
116 36 115 pm2.61dane 
 |-  ( ph -> ( A .- C ) = ( D .- F ) )