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 ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )