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 𝑃 = ( Base ‘ 𝐺 )
hypcgr.m = ( dist ‘ 𝐺 )
hypcgr.i 𝐼 = ( Itv ‘ 𝐺 )
hypcgr.g ( 𝜑𝐺 ∈ TarskiG )
hypcgr.h ( 𝜑𝐺 DimTarskiG≥ 2 )
hypcgr.a ( 𝜑𝐴𝑃 )
hypcgr.b ( 𝜑𝐵𝑃 )
hypcgr.c ( 𝜑𝐶𝑃 )
hypcgr.d ( 𝜑𝐷𝑃 )
hypcgr.e ( 𝜑𝐸𝑃 )
hypcgr.f ( 𝜑𝐹𝑃 )
hypcgr.1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
hypcgr.2 ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
hypcgr.3 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
hypcgr.4 ( 𝜑 → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
hypcgrlem2.b ( 𝜑𝐵 = 𝐸 )
hypcgrlem1.s 𝑆 = ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐷 ) ( LineG ‘ 𝐺 ) 𝐵 ) )
hypcgrlem1.a ( 𝜑𝐶 = 𝐹 )
Assertion hypcgrlem1 ( 𝜑 → ( 𝐴 𝐶 ) = ( 𝐷 𝐹 ) )

Proof

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