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