Metamath Proof Explorer

Theorem footexlem1

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 footexlem1 ( 𝜑 → 𝑋 ∈ 𝐴 )

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 22 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝑅 ) = ( 𝑌 − 𝑍 ) )
30 17 necomd ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
31 1 3 4 5 10 9 13 30 18 btwnlng3 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐹 𝐿 𝐸 ) )
32 1 3 4 5 9 10 13 17 31 lncom ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐸 𝐿 𝐹 ) )
33 32 16 eleqtrrd ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
34 nelne2 ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝑌 ≠ 𝐶 )
35 33 8 34 syl2anc ⊢ ( 𝜑 → 𝑌 ≠ 𝐶 )
36 35 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝑌 )
37 20 36 eqnetrrd ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ≠ 𝑌 )
38 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
39 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 )
40 1 2 3 4 38 5 11 39 13 mirinv ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) = 𝑌 ↔ 𝑅 = 𝑌 ) )
41 40 necon3bid ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ≠ 𝑌 ↔ 𝑅 ≠ 𝑌 ) )
42 37 41 mpbid ⊢ ( 𝜑 → 𝑅 ≠ 𝑌 )
43 42 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑅 )
44 1 2 3 5 13 11 13 14 29 43 tgcgrneq ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
45 44 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
46 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 )
47 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 )
48 1 2 3 4 38 5 14 46 23 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ∈ 𝑃 )
49 1 2 3 4 38 5 11 39 13 mirbtwn ⊢ ( 𝜑 → 𝑅 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) 𝐼 𝑌 ) )
50 20 oveq1d ⊢ ( 𝜑 → ( 𝐶 𝐼 𝑌 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) 𝐼 𝑌 ) )
51 49 50 eleqtrrd ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐶 𝐼 𝑌 ) )
52 1 2 3 5 7 11 13 23 42 51 24 tgbtwnouttr2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 𝐼 𝑄 ) )
53 1 2 3 5 7 13 23 52 tgbtwncom ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑄 𝐼 𝐶 ) )
54 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
55 20 oveq2d ⊢ ( 𝜑 → ( 𝐸 − 𝐶 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ) )
56 19 55 eqtrd ⊢ ( 𝜑 → ( 𝐸 − 𝑌 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ) )
57 1 2 3 4 38 5 9 11 13 israg ⊢ ( 𝜑 → ( ⟨“ 𝐸 𝑅 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐸 − 𝑌 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
58 56 57 mpbird ⊢ ( 𝜑 → ⟨“ 𝐸 𝑅 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
59 1 2 3 5 9 13 9 7 19 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑌 − 𝐸 ) = ( 𝐶 − 𝐸 ) )
60 25 59 eqtr2d ⊢ ( 𝜑 → ( 𝐶 − 𝐸 ) = ( 𝑌 − 𝑄 ) )
61 1 3 4 5 9 10 17 tglinerflx1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐸 𝐿 𝐹 ) )
62 61 16 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
63 nelne2 ⊢ ( ( 𝐸 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) → 𝐸 ≠ 𝐶 )
64 62 8 63 syl2anc ⊢ ( 𝜑 → 𝐸 ≠ 𝐶 )
65 64 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
66 1 2 3 5 7 9 13 23 60 65 tgcgrneq ⊢ ( 𝜑 → 𝑌 ≠ 𝑄 )
67 66 necomd ⊢ ( 𝜑 → 𝑄 ≠ 𝑌 )
68 1 2 3 5 11 13 23 24 tgbtwncom ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑄 𝐼 𝑅 ) )
69 1 2 3 5 13 23 13 9 25 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑄 − 𝑌 ) = ( 𝐸 − 𝑌 ) )
70 1 2 3 5 23 9 axtgcgrrflx ⊢ ( 𝜑 → ( 𝑄 − 𝐸 ) = ( 𝐸 − 𝑄 ) )
71 25 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝐸 ) = ( 𝑌 − 𝑄 ) )
72 1 2 3 5 23 13 11 9 13 14 9 23 67 68 21 69 29 70 71 axtg5seg ⊢ ( 𝜑 → ( 𝑅 − 𝐸 ) = ( 𝑍 − 𝑄 ) )
73 1 2 3 5 11 9 14 23 72 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐸 − 𝑅 ) = ( 𝑄 − 𝑍 ) )
74 1 2 3 5 13 11 13 14 29 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑅 − 𝑌 ) = ( 𝑍 − 𝑌 ) )
75 1 2 54 5 9 11 13 23 14 13 73 74 71 trgcgr ⊢ ( 𝜑 → ⟨“ 𝐸 𝑅 𝑌 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑄 𝑍 𝑌 ”⟩ )
76 1 2 3 4 38 5 9 11 13 54 23 14 13 58 75 ragcgr ⊢ ( 𝜑 → ⟨“ 𝑄 𝑍 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
77 1 2 3 4 38 5 23 14 13 76 ragcom ⊢ ( 𝜑 → ⟨“ 𝑌 𝑍 𝑄 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
78 1 2 3 4 38 5 13 14 23 israg ⊢ ( 𝜑 → ( ⟨“ 𝑌 𝑍 𝑄 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑌 − 𝑄 ) = ( 𝑌 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ) ) )
79 77 78 mpbid ⊢ ( 𝜑 → ( 𝑌 − 𝑄 ) = ( 𝑌 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) ) )
80 27 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝐶 ) = ( 𝑌 − 𝐷 ) )
81 eqidd ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ 𝑄 ) )
82 1 2 3 4 38 5 46 47 23 48 13 7 15 14 12 53 26 79 80 81 28 krippen ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑍 𝐼 𝑋 ) )
83 1 3 4 5 14 13 12 45 82 btwnlng3 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) )
84 1 3 4 5 13 14 12 44 83 lncom ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
85 19 eqcomd ⊢ ( 𝜑 → ( 𝐸 − 𝐶 ) = ( 𝐸 − 𝑌 ) )
86 1 2 3 5 9 7 9 13 85 64 tgcgrneq ⊢ ( 𝜑 → 𝐸 ≠ 𝑌 )
87 1 3 4 5 9 13 14 86 21 btwnlng3 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐸 𝐿 𝑌 ) )
88 1 3 4 5 9 13 86 86 6 62 33 tglinethru ⊢ ( 𝜑 → 𝐴 = ( 𝐸 𝐿 𝑌 ) )
89 87 88 eleqtrrd ⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
90 1 3 4 5 13 14 44 44 6 33 89 tglinethru ⊢ ( 𝜑 → 𝐴 = ( 𝑌 𝐿 𝑍 ) )
91 84 90 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )