Metamath Proof Explorer

Theorem footexlem2

Description: Lemma for footex . (Contributed by Thierry Arnoux, 19-Oct-2019) (Revised by Thierry Arnoux, 1-Jul-2023)

Ref Expression
Hypotheses isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isperp.d ⊢ − = ( dist ‘ 𝐺 )
isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
foot.x ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
foot.y ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
footexlem.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
footexlem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
footexlem.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
footexlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
footexlem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
footexlem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
footexlem.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
footexlem.1 ⊢ ( 𝜑 → 𝐴 = ( 𝐸 𝐿 𝐹 ) )
footexlem.2 ⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
footexlem.3 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 𝐼 𝑌 ) )
footexlem.4 ⊢ ( 𝜑 → ( 𝐸 − 𝑌 ) = ( 𝐸 − 𝐶 ) )
footexlem.5 ⊢ ( 𝜑 → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) )
footexlem.6 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐸 𝐼 𝑍 ) )
footexlem.7 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑌 − 𝑅 ) )
footexlem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
footexlem.8 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑅 𝐼 𝑄 ) )
footexlem.9 ⊢ ( 𝜑 → ( 𝑌 − 𝑄 ) = ( 𝑌 − 𝐸 ) )
footexlem.10 ⊢ ( 𝜑 → 𝑌 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) 𝐼 𝐷 ) )
footexlem.11 ⊢ ( 𝜑 → ( 𝑌 − 𝐷 ) = ( 𝑌 − 𝐶 ) )
footexlem.12 ⊢ ( 𝜑 → 𝐷 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) )
Assertion footexlem2 ( 𝜑 → ( 𝐶 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) 𝐴 )

Proof

Step Hyp Ref Expression
1 isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isperp.d ⊢ − = ( dist ‘ 𝐺 )
3 isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 foot.x ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 foot.y ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
9 footexlem.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 footexlem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 footexlem.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
12 footexlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
13 footexlem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
14 footexlem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
15 footexlem.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
16 footexlem.1 ⊢ ( 𝜑 → 𝐴 = ( 𝐸 𝐿 𝐹 ) )
17 footexlem.2 ⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
18 footexlem.3 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 𝐼 𝑌 ) )
19 footexlem.4 ⊢ ( 𝜑 → ( 𝐸 − 𝑌 ) = ( 𝐸 − 𝐶 ) )
20 footexlem.5 ⊢ ( 𝜑 → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) )
21 footexlem.6 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐸 𝐼 𝑍 ) )
22 footexlem.7 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑌 − 𝑅 ) )
23 footexlem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
24 footexlem.8 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑅 𝐼 𝑄 ) )
25 footexlem.9 ⊢ ( 𝜑 → ( 𝑌 − 𝑄 ) = ( 𝑌 − 𝐸 ) )
26 footexlem.10 ⊢ ( 𝜑 → 𝑌 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) 𝐼 𝐷 ) )
27 footexlem.11 ⊢ ( 𝜑 → ( 𝑌 − 𝐷 ) = ( 𝑌 − 𝐶 ) )
28 footexlem.12 ⊢ ( 𝜑 → 𝐷 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) )
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 footexlem1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
30 nelne2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝑋 ≠ 𝐶 )
31 29 8 30 syl2anc ⊢ ( 𝜑 → 𝑋 ≠ 𝐶 )
32 31 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝑋 )
33 1 3 4 5 7 12 32 tgelrnln ⊢ ( 𝜑 → ( 𝐶 𝐿 𝑋 ) ∈ ran 𝐿 )
34 1 3 4 5 7 12 32 tglinerflx2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 𝐿 𝑋 ) )
35 34 29 elind ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐶 𝐿 𝑋 ) ∩ 𝐴 ) )
36 1 3 4 5 7 12 32 tglinerflx1 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐶 𝐿 𝑋 ) )
37 17 necomd ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
38 1 3 4 5 10 9 13 37 18 btwnlng3 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐹 𝐿 𝐸 ) )
39 1 3 4 5 9 10 13 17 38 lncom ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐸 𝐿 𝐹 ) )
40 39 16 eleqtrrd ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
41 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
42 5 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐺 ∈ TarskiG )
43 9 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐸 ∈ 𝑃 )
44 13 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 ∈ 𝑃 )
45 11 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑅 ∈ 𝑃 )
46 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐶 ∈ 𝑃 )
47 eqidd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐶 = 𝐶 )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 = 𝑋 )
49 eqidd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐸 = 𝐸 )
50 47 48 49 s3eqd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝐶 𝑌 𝐸 ”⟩ = ⟨“ 𝐶 𝑋 𝐸 ”⟩ )
51 12 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑋 ∈ 𝑃 )
52 14 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑍 ∈ 𝑃 )
53 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 )
54 1 2 3 4 41 5 14 53 23 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ∈ 𝑃 )
55 1 2 3 5 9 13 9 7 19 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑌 − 𝐸 ) = ( 𝐶 − 𝐸 ) )
56 25 55 eqtr2d ⊢ ( 𝜑 → ( 𝐶 − 𝐸 ) = ( 𝑌 − 𝑄 ) )
57 1 3 4 5 9 10 17 tglinerflx1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐸 𝐿 𝐹 ) )
58 57 16 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
59 nelne2 ⊢ ( ( 𝐸 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝐸 ≠ 𝐶 )
60 58 8 59 syl2anc ⊢ ( 𝜑 → 𝐸 ≠ 𝐶 )
61 60 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
62 1 2 3 5 7 9 13 23 56 61 tgcgrneq ⊢ ( 𝜑 → 𝑌 ≠ 𝑄 )
63 62 necomd ⊢ ( 𝜑 → 𝑄 ≠ 𝑌 )
64 nelne2 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝑌 ≠ 𝐶 )
65 40 8 64 syl2anc ⊢ ( 𝜑 → 𝑌 ≠ 𝐶 )
66 65 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝑌 )
67 20 66 eqnetrrd ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ≠ 𝑌 )
68 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 )
69 1 2 3 4 41 5 11 68 13 mirinv ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) = 𝑌 ↔ 𝑅 = 𝑌 ) )
70 69 necon3bid ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ≠ 𝑌 ↔ 𝑅 ≠ 𝑌 ) )
71 67 70 mpbid ⊢ ( 𝜑 → 𝑅 ≠ 𝑌 )
72 1 2 3 4 41 5 11 68 13 mirbtwn ⊢ ( 𝜑 → 𝑅 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) 𝐼 𝑌 ) )
73 20 oveq1d ⊢ ( 𝜑 → ( 𝐶 𝐼 𝑌 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) 𝐼 𝑌 ) )
74 72 73 eleqtrrd ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐶 𝐼 𝑌 ) )
75 1 2 3 5 7 11 13 23 71 74 24 tgbtwnouttr2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 𝐼 𝑄 ) )
76 1 2 3 5 7 13 23 75 tgbtwncom ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑄 𝐼 𝐶 ) )
77 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
78 20 oveq2d ⊢ ( 𝜑 → ( 𝐸 − 𝐶 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ) )
79 19 78 eqtrd ⊢ ( 𝜑 → ( 𝐸 − 𝑌 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ) )
80 1 2 3 4 41 5 9 11 13 israg ⊢ ( 𝜑 → ( ⟨“ 𝐸 𝑅 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐸 − 𝑌 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
81 79 80 mpbird ⊢ ( 𝜑 → ⟨“ 𝐸 𝑅 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
82 1 2 3 5 11 13 23 24 tgbtwncom ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑄 𝐼 𝑅 ) )
83 1 2 3 5 13 23 13 9 25 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑄 − 𝑌 ) = ( 𝐸 − 𝑌 ) )
84 22 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝑅 ) = ( 𝑌 − 𝑍 ) )
85 1 2 3 5 23 9 axtgcgrrflx ⊢ ( 𝜑 → ( 𝑄 − 𝐸 ) = ( 𝐸 − 𝑄 ) )
86 25 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝐸 ) = ( 𝑌 − 𝑄 ) )
87 1 2 3 5 23 13 11 9 13 14 9 23 63 82 21 83 84 85 86 axtg5seg ⊢ ( 𝜑 → ( 𝑅 − 𝐸 ) = ( 𝑍 − 𝑄 ) )
88 1 2 3 5 11 9 14 23 87 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐸 − 𝑅 ) = ( 𝑄 − 𝑍 ) )
89 1 2 3 5 13 11 13 14 84 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑅 − 𝑌 ) = ( 𝑍 − 𝑌 ) )
90 1 2 77 5 9 11 13 23 14 13 88 89 86 trgcgr ⊢ ( 𝜑 → ⟨“ 𝐸 𝑅 𝑌 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑄 𝑍 𝑌 ”⟩ )
91 1 2 3 4 41 5 9 11 13 77 23 14 13 81 90 ragcgr ⊢ ( 𝜑 → ⟨“ 𝑄 𝑍 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
92 1 2 3 4 41 5 23 14 13 91 ragcom ⊢ ( 𝜑 → ⟨“ 𝑌 𝑍 𝑄 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
93 1 2 3 4 41 5 13 14 23 israg ⊢ ( 𝜑 → ( ⟨“ 𝑌 𝑍 𝑄 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑌 − 𝑄 ) = ( 𝑌 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ) ) )
94 92 93 mpbid ⊢ ( 𝜑 → ( 𝑌 − 𝑄 ) = ( 𝑌 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ) )
95 1 2 3 5 13 23 13 54 94 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑄 − 𝑌 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) − 𝑌 ) )
96 27 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝐶 ) = ( 𝑌 − 𝐷 ) )
97 1 2 3 4 41 5 14 53 23 mircgr ⊢ ( 𝜑 → ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ) = ( 𝑍 − 𝑄 ) )
98 97 eqcomd ⊢ ( 𝜑 → ( 𝑍 − 𝑄 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ) )
99 1 2 3 5 14 23 14 54 98 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑄 − 𝑍 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) − 𝑍 ) )
100 eqidd ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑌 − 𝑍 ) )
101 1 2 3 5 23 13 7 54 13 15 14 14 63 76 26 95 96 99 100 axtg5seg ⊢ ( 𝜑 → ( 𝐶 − 𝑍 ) = ( 𝐷 − 𝑍 ) )
102 1 2 3 5 7 14 15 14 101 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑍 − 𝐶 ) = ( 𝑍 − 𝐷 ) )
103 28 oveq2d ⊢ ( 𝜑 → ( 𝑍 − 𝐷 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) ) )
104 102 103 eqtrd ⊢ ( 𝜑 → ( 𝑍 − 𝐶 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) ) )
105 1 2 3 4 41 5 14 12 7 israg ⊢ ( 𝜑 → ( ⟨“ 𝑍 𝑋 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑍 − 𝐶 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) ) ) )
106 104 105 mpbird ⊢ ( 𝜑 → ⟨“ 𝑍 𝑋 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝑍 𝑋 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
108 71 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑅 )
109 1 2 3 5 13 11 13 14 84 108 tgcgrneq ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
110 109 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑍 ≠ 𝑌 )
112 111 48 neeqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑍 ≠ 𝑋 )
113 19 eqcomd ⊢ ( 𝜑 → ( 𝐸 − 𝐶 ) = ( 𝐸 − 𝑌 ) )
114 113 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ( 𝐸 − 𝐶 ) = ( 𝐸 − 𝑌 ) )
115 60 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐸 ≠ 𝐶 )
116 1 2 3 42 43 46 43 44 114 115 tgcgrneq ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐸 ≠ 𝑌 )
117 116 necomd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 ≠ 𝐸 )
118 1 2 3 5 9 7 9 13 113 60 tgcgrneq ⊢ ( 𝜑 → 𝐸 ≠ 𝑌 )
119 1 3 4 5 9 13 14 118 21 btwnlng3 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐸 𝐿 𝑌 ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑍 ∈ ( 𝐸 𝐿 𝑌 ) )
121 1 3 4 42 44 43 52 117 120 lncom ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑍 ∈ ( 𝑌 𝐿 𝐸 ) )
122 48 oveq1d ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ( 𝑌 𝐿 𝐸 ) = ( 𝑋 𝐿 𝐸 ) )
123 121 122 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑍 ∈ ( 𝑋 𝐿 𝐸 ) )
124 123 orcd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝐸 ) ∨ 𝑋 = 𝐸 ) )
125 1 2 3 4 41 42 52 51 46 43 107 112 124 ragcol ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝐸 𝑋 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
126 1 2 3 4 41 42 43 51 46 125 ragcom ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝐶 𝑋 𝐸 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
127 50 126 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝐶 𝑌 𝐸 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
128 66 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐶 ≠ 𝑌 )
129 1 2 3 5 7 11 13 74 tgbtwncom ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑌 𝐼 𝐶 ) )
130 1 4 3 5 13 11 7 129 btwncolg3 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝑌 𝐿 𝑅 ) ∨ 𝑌 = 𝑅 ) )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ( 𝐶 ∈ ( 𝑌 𝐿 𝑅 ) ∨ 𝑌 = 𝑅 ) )
132 1 2 3 4 41 42 46 44 43 45 127 128 131 ragcol ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝑅 𝑌 𝐸 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
133 1 2 3 4 41 42 45 44 43 132 ragcom ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝐸 𝑌 𝑅 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
134 81 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ⟨“ 𝐸 𝑅 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
135 1 2 3 4 41 42 43 44 45 133 134 ragflat ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 = 𝑅 )
136 108 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 ≠ 𝑅 )
137 136 neneqd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ¬ 𝑌 = 𝑅 )
138 135 137 pm2.65da ⊢ ( 𝜑 → ¬ 𝑌 = 𝑋 )
139 138 neqned ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
140 28 oveq2d ⊢ ( 𝜑 → ( 𝑌 − 𝐷 ) = ( 𝑌 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) ) )
141 96 140 eqtrd ⊢ ( 𝜑 → ( 𝑌 − 𝐶 ) = ( 𝑌 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) ) )
142 1 2 3 4 41 5 13 12 7 israg ⊢ ( 𝜑 → ( ⟨“ 𝑌 𝑋 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑌 − 𝐶 ) = ( 𝑌 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝐶 ) ) ) )
143 141 142 mpbird ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
144 1 2 3 4 41 5 13 12 7 143 ragcom ⊢ ( 𝜑 → ⟨“ 𝐶 𝑋 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
145 1 2 3 4 5 33 6 35 36 40 32 139 144 ragperp ⊢ ( 𝜑 → ( 𝐶 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) 𝐴 )