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	$$⊢P={\mathrm{Base}}_G$$
	isperp.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	isperp.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	isperp.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	isperp.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	isperp.a	$$⊢\phi \to A\in \mathrm{ran}L$$
	foot.x	$$⊢\phi \to C\in P$$
	foot.y	$$⊢\phi \to \neg C\in A$$
	footexlem.e	$$⊢\phi \to E\in P$$
	footexlem.f	$$⊢\phi \to F\in P$$
	footexlem.r	$$⊢\phi \to R\in P$$
	footexlem.x	$$⊢\phi \to X\in P$$
	footexlem.y	$$⊢\phi \to Y\in P$$
	footexlem.z	$$⊢\phi \to Z\in P$$
	footexlem.d	$$⊢\phi \to D\in P$$
	footexlem.1	$$⊢\phi \to A=ELF$$
	footexlem.2	$$⊢\phi \to E\ne F$$
	footexlem.3	$$⊢\phi \to E\in \left(FIY\right)$$
	footexlem.4	$$⊢\phi \to E\underset{\dot{}}{-}Y=E\underset{\dot{}}{-}C$$
	footexlem.5	$$⊢\phi \to C={pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)$$
	footexlem.6	$$⊢\phi \to Y\in \left(EIZ\right)$$
	footexlem.7	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}R$$
	footexlem.q	$$⊢\phi \to Q\in P$$
	footexlem.8	$$⊢\phi \to Y\in \left(RIQ\right)$$
	footexlem.9	$$⊢\phi \to Y\underset{\dot{}}{-}Q=Y\underset{\dot{}}{-}E$$
	footexlem.10	$$⊢\phi \to Y\in \left({pInv}_{𝒢}\left(G\right)\left(Z\right)\left(Q\right)ID\right)$$
	footexlem.11	$$⊢\phi \to Y\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}C$$
	footexlem.12	$$⊢\phi \to D={pInv}_{𝒢}\left(G\right)\left(X\right)\left(C\right)$$
Assertion	footexlem1	$$⊢\phi \to X\in A$$

Proof

Step	Hyp	Ref	Expression
1		isperp.p	$$⊢P={\mathrm{Base}}_G$$
2		isperp.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		isperp.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		isperp.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		isperp.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		isperp.a	$$⊢\phi \to A\in \mathrm{ran}L$$
7		foot.x	$$⊢\phi \to C\in P$$
8		foot.y	$$⊢\phi \to \neg C\in A$$
9		footexlem.e	$$⊢\phi \to E\in P$$
10		footexlem.f	$$⊢\phi \to F\in P$$
11		footexlem.r	$$⊢\phi \to R\in P$$
12		footexlem.x	$$⊢\phi \to X\in P$$
13		footexlem.y	$$⊢\phi \to Y\in P$$
14		footexlem.z	$$⊢\phi \to Z\in P$$
15		footexlem.d	$$⊢\phi \to D\in P$$
16		footexlem.1	$$⊢\phi \to A=ELF$$
17		footexlem.2	$$⊢\phi \to E\ne F$$
18		footexlem.3	$$⊢\phi \to E\in \left(FIY\right)$$
19		footexlem.4	$$⊢\phi \to E\underset{\dot{}}{-}Y=E\underset{\dot{}}{-}C$$
20		footexlem.5	$$⊢\phi \to C={pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)$$
21		footexlem.6	$$⊢\phi \to Y\in \left(EIZ\right)$$
22		footexlem.7	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}R$$
23		footexlem.q	$$⊢\phi \to Q\in P$$
24		footexlem.8	$$⊢\phi \to Y\in \left(RIQ\right)$$
25		footexlem.9	$$⊢\phi \to Y\underset{\dot{}}{-}Q=Y\underset{\dot{}}{-}E$$
26		footexlem.10	$$⊢\phi \to Y\in \left({pInv}_{𝒢}\left(G\right)\left(Z\right)\left(Q\right)ID\right)$$
27		footexlem.11	$$⊢\phi \to Y\underset{\dot{}}{-}D=Y\underset{\dot{}}{-}C$$
28		footexlem.12	$$⊢\phi \to D={pInv}_{𝒢}\left(G\right)\left(X\right)\left(C\right)$$
29	22	eqcomd	$$⊢\phi \to Y\underset{\dot{}}{-}R=Y\underset{\dot{}}{-}Z$$
30	17	necomd	$$⊢\phi \to F\ne E$$
31	1 3 4 5 10 9 13 30 18	btwnlng3	$$⊢\phi \to Y\in \left(FLE\right)$$
32	1 3 4 5 9 10 13 17 31	lncom	$$⊢\phi \to Y\in \left(ELF\right)$$
33	32 16	eleqtrrd	$$⊢\phi \to Y\in A$$
34		nelne2	$$⊢\left(Y\in A\wedge \neg C\in A\right)\to Y\ne C$$
35	33 8 34	syl2anc	$$⊢\phi \to Y\ne C$$
36	35	necomd	$$⊢\phi \to C\ne Y$$
37	20 36	eqnetrrd	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)\ne Y$$
38		eqid	$$⊢{pInv}_{𝒢}\left(G\right)={pInv}_{𝒢}\left(G\right)$$
39		eqid	$$⊢{pInv}_{𝒢}\left(G\right)\left(R\right)={pInv}_{𝒢}\left(G\right)\left(R\right)$$
40	1 2 3 4 38 5 11 39 13	mirinv	$$⊢\phi \to \left({pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)=Y\leftrightarrow R=Y\right)$$
41	40	necon3bid	$$⊢\phi \to \left({pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)\ne Y\leftrightarrow R\ne Y\right)$$
42	37 41	mpbid	$$⊢\phi \to R\ne Y$$
43	42	necomd	$$⊢\phi \to Y\ne R$$
44	1 2 3 5 13 11 13 14 29 43	tgcgrneq	$$⊢\phi \to Y\ne Z$$
45	44	necomd	$$⊢\phi \to Z\ne Y$$
46		eqid	$$⊢{pInv}_{𝒢}\left(G\right)\left(Z\right)={pInv}_{𝒢}\left(G\right)\left(Z\right)$$
47		eqid	$$⊢{pInv}_{𝒢}\left(G\right)\left(X\right)={pInv}_{𝒢}\left(G\right)\left(X\right)$$
48	1 2 3 4 38 5 14 46 23	mircl	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(Z\right)\left(Q\right)\in P$$
49	1 2 3 4 38 5 11 39 13	mirbtwn	$$⊢\phi \to R\in \left({pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)IY\right)$$
50	20	oveq1d	$$⊢\phi \to CIY={pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)IY$$
51	49 50	eleqtrrd	$$⊢\phi \to R\in \left(CIY\right)$$
52	1 2 3 5 7 11 13 23 42 51 24	tgbtwnouttr2	$$⊢\phi \to Y\in \left(CIQ\right)$$
53	1 2 3 5 7 13 23 52	tgbtwncom	$$⊢\phi \to Y\in \left(QIC\right)$$
54		eqid	$$⊢{\sim }_{𝒢}\left(G\right)={\sim }_{𝒢}\left(G\right)$$
55	20	oveq2d	$$⊢\phi \to E\underset{\dot{}}{-}C=E\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)$$
56	19 55	eqtrd	$$⊢\phi \to E\underset{\dot{}}{-}Y=E\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)$$
57	1 2 3 4 38 5 9 11 13	israg	$$⊢\phi \to \left(⟨“ERY”⟩\in {∟}_{𝒢}\left(G\right)\leftrightarrow E\underset{\dot{}}{-}Y=E\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(R\right)\left(Y\right)\right)$$
58	56 57	mpbird	$$⊢\phi \to ⟨“ERY”⟩\in {∟}_{𝒢}\left(G\right)$$
59	1 2 3 5 9 13 9 7 19	tgcgrcomlr	$$⊢\phi \to Y\underset{\dot{}}{-}E=C\underset{\dot{}}{-}E$$
60	25 59	eqtr2d	$$⊢\phi \to C\underset{\dot{}}{-}E=Y\underset{\dot{}}{-}Q$$
61	1 3 4 5 9 10 17	tglinerflx1	$$⊢\phi \to E\in \left(ELF\right)$$
62	61 16	eleqtrrd	$$⊢\phi \to E\in A$$
63		nelne2	$$⊢\left(E\in A\wedge \neg C\in A\right)\to E\ne C$$
64	62 8 63	syl2anc	$$⊢\phi \to E\ne C$$
65	64	necomd	$$⊢\phi \to C\ne E$$
66	1 2 3 5 7 9 13 23 60 65	tgcgrneq	$$⊢\phi \to Y\ne Q$$
67	66	necomd	$$⊢\phi \to Q\ne Y$$
68	1 2 3 5 11 13 23 24	tgbtwncom	$$⊢\phi \to Y\in \left(QIR\right)$$
69	1 2 3 5 13 23 13 9 25	tgcgrcomlr	$$⊢\phi \to Q\underset{\dot{}}{-}Y=E\underset{\dot{}}{-}Y$$
70	1 2 3 5 23 9	axtgcgrrflx	$$⊢\phi \to Q\underset{\dot{}}{-}E=E\underset{\dot{}}{-}Q$$
71	25	eqcomd	$$⊢\phi \to Y\underset{\dot{}}{-}E=Y\underset{\dot{}}{-}Q$$
72	1 2 3 5 23 13 11 9 13 14 9 23 67 68 21 69 29 70 71	axtg5seg	$$⊢\phi \to R\underset{\dot{}}{-}E=Z\underset{\dot{}}{-}Q$$
73	1 2 3 5 11 9 14 23 72	tgcgrcomlr	$$⊢\phi \to E\underset{\dot{}}{-}R=Q\underset{\dot{}}{-}Z$$
74	1 2 3 5 13 11 13 14 29	tgcgrcomlr	$$⊢\phi \to R\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}Y$$
75	1 2 54 5 9 11 13 23 14 13 73 74 71	trgcgr	$$⊢\phi \to ⟨“ERY”⟩{\sim }_{𝒢}\left(G\right)⟨“QZY”⟩$$
76	1 2 3 4 38 5 9 11 13 54 23 14 13 58 75	ragcgr	$$⊢\phi \to ⟨“QZY”⟩\in {∟}_{𝒢}\left(G\right)$$
77	1 2 3 4 38 5 23 14 13 76	ragcom	$$⊢\phi \to ⟨“YZQ”⟩\in {∟}_{𝒢}\left(G\right)$$
78	1 2 3 4 38 5 13 14 23	israg	$$⊢\phi \to \left(⟨“YZQ”⟩\in {∟}_{𝒢}\left(G\right)\leftrightarrow Y\underset{\dot{}}{-}Q=Y\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(Z\right)\left(Q\right)\right)$$
79	77 78	mpbid	$$⊢\phi \to Y\underset{\dot{}}{-}Q=Y\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(Z\right)\left(Q\right)$$
80	27	eqcomd	$$⊢\phi \to Y\underset{\dot{}}{-}C=Y\underset{\dot{}}{-}D$$
81		eqidd	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(Z\right)\left(Q\right)={pInv}_{𝒢}\left(G\right)\left(Z\right)\left(Q\right)$$
82	1 2 3 4 38 5 46 47 23 48 13 7 15 14 12 53 26 79 80 81 28	krippen	$$⊢\phi \to Y\in \left(ZIX\right)$$
83	1 3 4 5 14 13 12 45 82	btwnlng3	$$⊢\phi \to X\in \left(ZLY\right)$$
84	1 3 4 5 13 14 12 44 83	lncom	$$⊢\phi \to X\in \left(YLZ\right)$$
85	19	eqcomd	$$⊢\phi \to E\underset{\dot{}}{-}C=E\underset{\dot{}}{-}Y$$
86	1 2 3 5 9 7 9 13 85 64	tgcgrneq	$$⊢\phi \to E\ne Y$$
87	1 3 4 5 9 13 14 86 21	btwnlng3	$$⊢\phi \to Z\in \left(ELY\right)$$
88	1 3 4 5 9 13 86 86 6 62 33	tglinethru	$$⊢\phi \to A=ELY$$
89	87 88	eleqtrrd	$$⊢\phi \to Z\in A$$
90	1 3 4 5 13 14 44 44 6 33 89	tglinethru	$$⊢\phi \to A=YLZ$$
91	84 90	eleqtrrd	$$⊢\phi \to X\in A$$