Theorem footexlem2 28700

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

Hypotheses

Ref	Expression
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

Ref	Expression
footexlem2	⊢ (𝜑 → (𝐶𝐿𝑋)(⟂G‘𝐺)𝐴)

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 28699	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
30		nelne2 3023	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝑋 ≠ 𝐶)
31	29, 9, 30	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝐶)
32	31	necomd 2980	. . 3 ⊢ (𝜑 → 𝐶 ≠ 𝑋)
33	1, 3, 4, 5, 6, 7, 32	tgelrnln 28610	. 2 ⊢ (𝜑 → (𝐶𝐿𝑋) ∈ ran 𝐿)
34	1, 3, 4, 5, 6, 7, 32	tglinerflx2 28614	. . 3 ⊢ (𝜑 → 𝑋 ∈ (𝐶𝐿𝑋))
35	34, 29	elind 4159	. 2 ⊢ (𝜑 → 𝑋 ∈ ((𝐶𝐿𝑋) ∩ 𝐴))
36	1, 3, 4, 5, 6, 7, 32	tglinerflx1 28613	. 2 ⊢ (𝜑 → 𝐶 ∈ (𝐶𝐿𝑋))
37	17	necomd 2980	. . . . 5 ⊢ (𝜑 → 𝐹 ≠ 𝐸)
38	1, 3, 4, 5, 11, 10, 13, 37, 18	btwnlng3 28601	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝐹𝐿𝐸))
39	1, 3, 4, 5, 10, 11, 13, 17, 38	lncom 28602	. . 3 ⊢ (𝜑 → 𝑌 ∈ (𝐸𝐿𝐹))
40	39, 16	eleqtrrd 2831	. 2 ⊢ (𝜑 → 𝑌 ∈ 𝐴)
41		eqid 2729	. . . . 5 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
42	5	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐺 ∈ TarskiG)
43	10	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 ∈ 𝑃)
44	13	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 ∈ 𝑃)
45	12	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑅 ∈ 𝑃)
46	6	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐶 ∈ 𝑃)
47		eqidd 2730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐶 = 𝐶)
48		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑋)
49		eqidd 2730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 = 𝐸)
50	47, 48, 49	s3eqd 14806	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝐶𝑌𝐸”⟩ = ⟨“𝐶𝑋𝐸”⟩)
51	7	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑋 ∈ 𝑃)
52	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ 𝑃)
53		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ ((pInvG‘𝐺)‘𝑍) = ((pInvG‘𝐺)‘𝑍)
54	1, 2, 3, 4, 41, 5, 14, 53, 23	mircl 28641	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑍)‘𝑄) ∈ 𝑃)
55	1, 2, 3, 5, 10, 13, 10, 6, 19	tgcgrcomlr 28460	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑌 − 𝐸) = (𝐶 − 𝐸))
56	25, 55	eqtr2d 2765	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 − 𝐸) = (𝑌 − 𝑄))
57	1, 3, 4, 5, 10, 11, 17	tglinerflx1 28613	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐸 ∈ (𝐸𝐿𝐹))
58	57, 16	eleqtrrd 2831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐸 ∈ 𝐴)
59		nelne2 3023	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐸 ≠ 𝐶)
60	58, 9, 59	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ≠ 𝐶)
61	60	necomd 2980	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ≠ 𝐸)
62	1, 2, 3, 5, 6, 10, 13, 23, 56, 61	tgcgrneq 28463	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ≠ 𝑄)
63	62	necomd 2980	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ≠ 𝑌)
64		nelne2 3023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑌 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝑌 ≠ 𝐶)
65	40, 9, 64	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 ≠ 𝐶)
66	65	necomd 2980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐶 ≠ 𝑌)
67	20, 66	eqnetrrd 2993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌)
68		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((pInvG‘𝐺)‘𝑅) = ((pInvG‘𝐺)‘𝑅)
69	1, 2, 3, 4, 41, 5, 12, 68, 13	mirinv 28646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) = 𝑌 ↔ 𝑅 = 𝑌))
70	69	necon3bid 2969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌 ↔ 𝑅 ≠ 𝑌))
71	67, 70	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑅 ≠ 𝑌)
72	1, 2, 3, 4, 41, 5, 12, 68, 13	mirbtwn 28638	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑅 ∈ ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌))
73	20	oveq1d 7384	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶𝐼𝑌) = ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌))
74	72, 73	eleqtrrd 2831	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑅 ∈ (𝐶𝐼𝑌))
75	1, 2, 3, 5, 6, 12, 13, 23, 71, 74, 24	tgbtwnouttr2 28475	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝑄))
76	1, 2, 3, 5, 6, 13, 23, 75	tgbtwncom 28468	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (𝑄𝐼𝐶))
77		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
78	20	oveq2d 7385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 − 𝐶) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌)))
79	19, 78	eqtrd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 − 𝑌) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌)))
80	1, 2, 3, 4, 41, 5, 10, 12, 13	israg 28677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (⟨“𝐸𝑅𝑌”⟩ ∈ (∟G‘𝐺) ↔ (𝐸 − 𝑌) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌))))
81	79, 80	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ⟨“𝐸𝑅𝑌”⟩ ∈ (∟G‘𝐺))
82	1, 2, 3, 5, 12, 13, 23, 24	tgbtwncom 28468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑌 ∈ (𝑄𝐼𝑅))
83	1, 2, 3, 5, 13, 23, 13, 10, 25	tgcgrcomlr 28460	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄 − 𝑌) = (𝐸 − 𝑌))
84	22	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑌 − 𝑅) = (𝑌 − 𝑍))
85	1, 2, 3, 5, 23, 10	axtgcgrrflx 28442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄 − 𝐸) = (𝐸 − 𝑄))
86	25	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑌 − 𝐸) = (𝑌 − 𝑄))
87	1, 2, 3, 5, 23, 13, 12, 10, 13, 14, 10, 23, 63, 82, 21, 83, 84, 85, 86	axtg5seg 28445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑅 − 𝐸) = (𝑍 − 𝑄))
88	1, 2, 3, 5, 12, 10, 14, 23, 87	tgcgrcomlr 28460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 − 𝑅) = (𝑄 − 𝑍))
89	1, 2, 3, 5, 13, 12, 13, 14, 84	tgcgrcomlr 28460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑅 − 𝑌) = (𝑍 − 𝑌))
90	1, 2, 77, 5, 10, 12, 13, 23, 14, 13, 88, 89, 86	trgcgr 28496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ⟨“𝐸𝑅𝑌”⟩(cgrG‘𝐺)⟨“𝑄𝑍𝑌”⟩)
91	1, 2, 3, 4, 41, 5, 10, 12, 13, 77, 23, 14, 13, 81, 90	ragcgr 28687	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ⟨“𝑄𝑍𝑌”⟩ ∈ (∟G‘𝐺))
92	1, 2, 3, 4, 41, 5, 23, 14, 13, 91	ragcom 28678	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨“𝑌𝑍𝑄”⟩ ∈ (∟G‘𝐺))
93	1, 2, 3, 4, 41, 5, 13, 14, 23	israg 28677	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (⟨“𝑌𝑍𝑄”⟩ ∈ (∟G‘𝐺) ↔ (𝑌 − 𝑄) = (𝑌 − (((pInvG‘𝐺)‘𝑍)‘𝑄))))
94	92, 93	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − 𝑄) = (𝑌 − (((pInvG‘𝐺)‘𝑍)‘𝑄)))
95	1, 2, 3, 5, 13, 23, 13, 54, 94	tgcgrcomlr 28460	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 − 𝑌) = ((((pInvG‘𝐺)‘𝑍)‘𝑄) − 𝑌))
96	27	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 − 𝐶) = (𝑌 − 𝐷))
97	1, 2, 3, 4, 41, 5, 14, 53, 23	mircgr 28637	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 − (((pInvG‘𝐺)‘𝑍)‘𝑄)) = (𝑍 − 𝑄))
98	97	eqcomd 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍 − 𝑄) = (𝑍 − (((pInvG‘𝐺)‘𝑍)‘𝑄)))
99	1, 2, 3, 5, 14, 23, 14, 54, 98	tgcgrcomlr 28460	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄 − 𝑍) = ((((pInvG‘𝐺)‘𝑍)‘𝑄) − 𝑍))
100		eqidd 2730	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝑍))
101	1, 2, 3, 5, 23, 13, 6, 54, 13, 15, 14, 14, 63, 76, 26, 95, 96, 99, 100	axtg5seg 28445	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 − 𝑍) = (𝐷 − 𝑍))
102	1, 2, 3, 5, 6, 14, 15, 14, 101	tgcgrcomlr 28460	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑍 − 𝐶) = (𝑍 − 𝐷))
103	28	oveq2d 7385	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑍 − 𝐷) = (𝑍 − (((pInvG‘𝐺)‘𝑋)‘𝐶)))
104	102, 103	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 − 𝐶) = (𝑍 − (((pInvG‘𝐺)‘𝑋)‘𝐶)))
105	1, 2, 3, 4, 41, 5, 14, 7, 6	israg 28677	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨“𝑍𝑋𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐶) = (𝑍 − (((pInvG‘𝐺)‘𝑋)‘𝐶))))
106	104, 105	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨“𝑍𝑋𝐶”⟩ ∈ (∟G‘𝐺))
107	106	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝑍𝑋𝐶”⟩ ∈ (∟G‘𝐺))
108	71	necomd 2980	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ≠ 𝑅)
109	1, 2, 3, 5, 13, 12, 13, 14, 84, 108	tgcgrneq 28463	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
110	109	necomd 2980	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ≠ 𝑌)
111	110	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ≠ 𝑌)
112	111, 48	neeqtrd 2994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ≠ 𝑋)
113	19	eqcomd 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 − 𝐶) = (𝐸 − 𝑌))
114	113	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝐸 − 𝐶) = (𝐸 − 𝑌))
115	60	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 ≠ 𝐶)
116	1, 2, 3, 42, 43, 46, 43, 44, 114, 115	tgcgrneq 28463	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 ≠ 𝑌)
117	116	necomd 2980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 ≠ 𝐸)
118	1, 2, 3, 5, 10, 6, 10, 13, 113, 60	tgcgrneq 28463	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ≠ 𝑌)
119	1, 3, 4, 5, 10, 13, 14, 118, 21	btwnlng3 28601	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 ∈ (𝐸𝐿𝑌))
120	119	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ (𝐸𝐿𝑌))
121	1, 3, 4, 42, 44, 43, 52, 117, 120	lncom 28602	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ (𝑌𝐿𝐸))
122	48	oveq1d 7384	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝑌𝐿𝐸) = (𝑋𝐿𝐸))
123	121, 122	eleqtrd 2830	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ (𝑋𝐿𝐸))
124	123	orcd 873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝑍 ∈ (𝑋𝐿𝐸) ∨ 𝑋 = 𝐸))
125	1, 2, 3, 4, 41, 42, 52, 51, 46, 43, 107, 112, 124	ragcol 28679	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝐸𝑋𝐶”⟩ ∈ (∟G‘𝐺))
126	1, 2, 3, 4, 41, 42, 43, 51, 46, 125	ragcom 28678	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝐶𝑋𝐸”⟩ ∈ (∟G‘𝐺))
127	50, 126	eqeltrd 2828	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝐶𝑌𝐸”⟩ ∈ (∟G‘𝐺))
128	66	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐶 ≠ 𝑌)
129	1, 2, 3, 5, 6, 12, 13, 74	tgbtwncom 28468	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (𝑌𝐼𝐶))
130	1, 4, 3, 5, 13, 12, 6, 129	btwncolg3 28537	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ∈ (𝑌𝐿𝑅) ∨ 𝑌 = 𝑅))
131	130	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝐶 ∈ (𝑌𝐿𝑅) ∨ 𝑌 = 𝑅))
132	1, 2, 3, 4, 41, 42, 46, 44, 43, 45, 127, 128, 131	ragcol 28679	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝑅𝑌𝐸”⟩ ∈ (∟G‘𝐺))
133	1, 2, 3, 4, 41, 42, 45, 44, 43, 132	ragcom 28678	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝐸𝑌𝑅”⟩ ∈ (∟G‘𝐺))
134	81	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ⟨“𝐸𝑅𝑌”⟩ ∈ (∟G‘𝐺))
135	1, 2, 3, 4, 41, 42, 43, 44, 45, 133, 134	ragflat 28684	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑅)
136	108	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 ≠ 𝑅)
137	136	neneqd 2930	. . . 4 ⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ¬ 𝑌 = 𝑅)
138	135, 137	pm2.65da 816	. . 3 ⊢ (𝜑 → ¬ 𝑌 = 𝑋)
139	138	neqned 2932	. 2 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
140	28	oveq2d 7385	. . . . 5 ⊢ (𝜑 → (𝑌 − 𝐷) = (𝑌 − (((pInvG‘𝐺)‘𝑋)‘𝐶)))
141	96, 140	eqtrd 2764	. . . 4 ⊢ (𝜑 → (𝑌 − 𝐶) = (𝑌 − (((pInvG‘𝐺)‘𝑋)‘𝐶)))
142	1, 2, 3, 4, 41, 5, 13, 7, 6	israg 28677	. . . 4 ⊢ (𝜑 → (⟨“𝑌𝑋𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑌 − 𝐶) = (𝑌 − (((pInvG‘𝐺)‘𝑋)‘𝐶))))
143	141, 142	mpbird 257	. . 3 ⊢ (𝜑 → ⟨“𝑌𝑋𝐶”⟩ ∈ (∟G‘𝐺))
144	1, 2, 3, 4, 41, 5, 13, 7, 6, 143	ragcom 28678	. 2 ⊢ (𝜑 → ⟨“𝐶𝑋𝑌”⟩ ∈ (∟G‘𝐺))
145	1, 2, 3, 4, 5, 33, 8, 35, 36, 40, 32, 139, 144	ragperp 28697	1 ⊢ (𝜑 → (𝐶𝐿𝑋)(⟂G‘𝐺)𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5102  ran crn 5632  ‘cfv 6499  (class class class)co 7369  ⟨“cs3 14784  Basecbs 17155  distcds 17205  TarskiGcstrkg 28407  Itvcitv 28413  LineGclng 28414  cgrGccgrg 28490  pInvGcmir 28632  ∟Gcrag 28673  ⟂Gcperpg 28675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-oadd 8415  df-er 8648  df-map 8778  df-pm 8779  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-dju 9830  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-xnn0 12492  df-z 12506  df-uz 12770  df-fz 13445  df-fzo 13592  df-hash 14272  df-word 14455  df-concat 14512  df-s1 14537  df-s2 14790  df-s3 14791  df-trkgc 28428  df-trkgb 28429  df-trkgcb 28430  df-trkg 28433  df-cgrg 28491  df-leg 28563  df-mir 28633  df-rag 28674  df-perpg 28676

This theorem is referenced by:  footex  28701