footexlem2

	Ref	Expression
Hypotheses	isperp.p	$⊢ P = {Base}_{G}$
	isperp.d	$⊢ \underset{˙}{-} = dist (G)$
	isperp.i	$⊢ I = Itv (G)$
	isperp.l	$⊢ L = {Line}_{𝒢} (G)$
	isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	isperp.a	$⊢ φ \to A \in ran L$
	foot.x	$⊢ φ \to C \in P$
	foot.y	$⊢ φ \to \neg C \in A$
	footexlem.e	$⊢ φ \to E \in P$
	footexlem.f	$⊢ φ \to F \in P$
	footexlem.r	$⊢ φ \to R \in P$
	footexlem.x	$⊢ φ \to X \in P$
	footexlem.y	$⊢ φ \to Y \in P$
	footexlem.z	$⊢ φ \to Z \in P$
	footexlem.d	$⊢ φ \to D \in P$
	footexlem.1	$⊢ φ \to A = E L F$
	footexlem.2	$⊢ φ \to E \neq F$
	footexlem.3	$⊢ φ \to E \in (F I Y)$
	footexlem.4	$⊢ φ \to E \underset{˙}{-} Y = E \underset{˙}{-} C$
	footexlem.5	$⊢ φ \to C = {pInv}_{𝒢} (G) (R) (Y)$
	footexlem.6	$⊢ φ \to Y \in (E I Z)$
	footexlem.7	$⊢ φ \to Y \underset{˙}{-} Z = Y \underset{˙}{-} R$
	footexlem.q	$⊢ φ \to Q \in P$
	footexlem.8	$⊢ φ \to Y \in (R I Q)$
	footexlem.9	$⊢ φ \to Y \underset{˙}{-} Q = Y \underset{˙}{-} E$
	footexlem.10	$⊢ φ \to Y \in ({pInv}_{𝒢} (G) (Z) (Q) I D)$
	footexlem.11	$⊢ φ \to Y \underset{˙}{-} D = Y \underset{˙}{-} C$
	footexlem.12	$⊢ φ \to D = {pInv}_{𝒢} (G) (X) (C)$
Assertion	footexlem2	$⊢ φ \to (C L X) ⟂_{𝒢} (G) A$

Proof

Step	Hyp	Ref	Expression
1		isperp.p	$⊢ P = {Base}_{G}$
2		isperp.d	$⊢ \underset{˙}{-} = dist (G)$
3		isperp.i	$⊢ I = Itv (G)$
4		isperp.l	$⊢ L = {Line}_{𝒢} (G)$
5		isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		isperp.a	$⊢ φ \to A \in ran L$
7		foot.x	$⊢ φ \to C \in P$
8		foot.y	$⊢ φ \to \neg C \in A$
9		footexlem.e	$⊢ φ \to E \in P$
10		footexlem.f	$⊢ φ \to F \in P$
11		footexlem.r	$⊢ φ \to R \in P$
12		footexlem.x	$⊢ φ \to X \in P$
13		footexlem.y	$⊢ φ \to Y \in P$
14		footexlem.z	$⊢ φ \to Z \in P$
15		footexlem.d	$⊢ φ \to D \in P$
16		footexlem.1	$⊢ φ \to A = E L F$
17		footexlem.2	$⊢ φ \to E \neq F$
18		footexlem.3	$⊢ φ \to E \in (F I Y)$
19		footexlem.4	$⊢ φ \to E \underset{˙}{-} Y = E \underset{˙}{-} C$
20		footexlem.5	$⊢ φ \to C = {pInv}_{𝒢} (G) (R) (Y)$
21		footexlem.6	$⊢ φ \to Y \in (E I Z)$
22		footexlem.7	$⊢ φ \to Y \underset{˙}{-} Z = Y \underset{˙}{-} R$
23		footexlem.q	$⊢ φ \to Q \in P$
24		footexlem.8	$⊢ φ \to Y \in (R I Q)$
25		footexlem.9	$⊢ φ \to Y \underset{˙}{-} Q = Y \underset{˙}{-} E$
26		footexlem.10	$⊢ φ \to Y \in ({pInv}_{𝒢} (G) (Z) (Q) I D)$
27		footexlem.11	$⊢ φ \to Y \underset{˙}{-} D = Y \underset{˙}{-} C$
28		footexlem.12	$⊢ φ \to D = {pInv}_{𝒢} (G) (X) (C)$
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	$⊢ φ \to X \in A$
30		nelne2	$⊢ (X \in A \land \neg C \in A) \to X \neq C$
31	29 8 30	syl2anc	$⊢ φ \to X \neq C$
32	31	necomd	$⊢ φ \to C \neq X$
33	1 3 4 5 7 12 32	tgelrnln	$⊢ φ \to C L X \in ran L$
34	1 3 4 5 7 12 32	tglinerflx2	$⊢ φ \to X \in (C L X)$
35	34 29	elind	$⊢ φ \to X \in ((C L X) \cap A)$
36	1 3 4 5 7 12 32	tglinerflx1	$⊢ φ \to C \in (C L X)$
37	17	necomd	$⊢ φ \to F \neq E$
38	1 3 4 5 10 9 13 37 18	btwnlng3	$⊢ φ \to Y \in (F L E)$
39	1 3 4 5 9 10 13 17 38	lncom	$⊢ φ \to Y \in (E L F)$
40	39 16	eleqtrrd	$⊢ φ \to Y \in A$
41		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
42	5	adantr	$⊢ (φ \land Y = X) \to G \in 𝒢_{Tarski}$
43	9	adantr	$⊢ (φ \land Y = X) \to E \in P$
44	13	adantr	$⊢ (φ \land Y = X) \to Y \in P$
45	11	adantr	$⊢ (φ \land Y = X) \to R \in P$
46	7	adantr	$⊢ (φ \land Y = X) \to C \in P$
47		eqidd	$⊢ (φ \land Y = X) \to C = C$
48		simpr	$⊢ (φ \land Y = X) \to Y = X$
49		eqidd	$⊢ (φ \land Y = X) \to E = E$
50	47 48 49	s3eqd	$⊢ (φ \land Y = X) \to ⟨“ C Y E ”⟩ = ⟨“ C X E ”⟩$
51	12	adantr	$⊢ (φ \land Y = X) \to X \in P$
52	14	adantr	$⊢ (φ \land Y = X) \to Z \in P$
53		eqid	$⊢ {pInv}_{𝒢} (G) (Z) = {pInv}_{𝒢} (G) (Z)$
54	1 2 3 4 41 5 14 53 23	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (Z) (Q) \in P$
55	1 2 3 5 9 13 9 7 19	tgcgrcomlr	$⊢ φ \to Y \underset{˙}{-} E = C \underset{˙}{-} E$
56	25 55	eqtr2d	$⊢ φ \to C \underset{˙}{-} E = Y \underset{˙}{-} Q$
57	1 3 4 5 9 10 17	tglinerflx1	$⊢ φ \to E \in (E L F)$
58	57 16	eleqtrrd	$⊢ φ \to E \in A$
59		nelne2	$⊢ (E \in A \land \neg C \in A) \to E \neq C$
60	58 8 59	syl2anc	$⊢ φ \to E \neq C$
61	60	necomd	$⊢ φ \to C \neq E$
62	1 2 3 5 7 9 13 23 56 61	tgcgrneq	$⊢ φ \to Y \neq Q$
63	62	necomd	$⊢ φ \to Q \neq Y$
64		nelne2	$⊢ (Y \in A \land \neg C \in A) \to Y \neq C$
65	40 8 64	syl2anc	$⊢ φ \to Y \neq C$
66	65	necomd	$⊢ φ \to C \neq Y$
67	20 66	eqnetrrd	$⊢ φ \to {pInv}_{𝒢} (G) (R) (Y) \neq Y$
68		eqid	$⊢ {pInv}_{𝒢} (G) (R) = {pInv}_{𝒢} (G) (R)$
69	1 2 3 4 41 5 11 68 13	mirinv	$⊢ φ \to ({pInv}_{𝒢} (G) (R) (Y) = Y \leftrightarrow R = Y)$
70	69	necon3bid	$⊢ φ \to ({pInv}_{𝒢} (G) (R) (Y) \neq Y \leftrightarrow R \neq Y)$
71	67 70	mpbid	$⊢ φ \to R \neq Y$
72	1 2 3 4 41 5 11 68 13	mirbtwn	$⊢ φ \to R \in ({pInv}_{𝒢} (G) (R) (Y) I Y)$
73	20	oveq1d	$⊢ φ \to C I Y = {pInv}_{𝒢} (G) (R) (Y) I Y$
74	72 73	eleqtrrd	$⊢ φ \to R \in (C I Y)$
75	1 2 3 5 7 11 13 23 71 74 24	tgbtwnouttr2	$⊢ φ \to Y \in (C I Q)$
76	1 2 3 5 7 13 23 75	tgbtwncom	$⊢ φ \to Y \in (Q I C)$
77		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
78	20	oveq2d	$⊢ φ \to E \underset{˙}{-} C = E \underset{˙}{-} {pInv}_{𝒢} (G) (R) (Y)$
79	19 78	eqtrd	$⊢ φ \to E \underset{˙}{-} Y = E \underset{˙}{-} {pInv}_{𝒢} (G) (R) (Y)$
80	1 2 3 4 41 5 9 11 13	israg	$⊢ φ \to (⟨“ E R Y ”⟩ \in ∟_{𝒢} (G) \leftrightarrow E \underset{˙}{-} Y = E \underset{˙}{-} {pInv}_{𝒢} (G) (R) (Y))$
81	79 80	mpbird	$⊢ φ \to ⟨“ E R Y ”⟩ \in ∟_{𝒢} (G)$
82	1 2 3 5 11 13 23 24	tgbtwncom	$⊢ φ \to Y \in (Q I R)$
83	1 2 3 5 13 23 13 9 25	tgcgrcomlr	$⊢ φ \to Q \underset{˙}{-} Y = E \underset{˙}{-} Y$
84	22	eqcomd	$⊢ φ \to Y \underset{˙}{-} R = Y \underset{˙}{-} Z$
85	1 2 3 5 23 9	axtgcgrrflx	$⊢ φ \to Q \underset{˙}{-} E = E \underset{˙}{-} Q$
86	25	eqcomd	$⊢ φ \to Y \underset{˙}{-} E = Y \underset{˙}{-} Q$
87	1 2 3 5 23 13 11 9 13 14 9 23 63 82 21 83 84 85 86	axtg5seg	$⊢ φ \to R \underset{˙}{-} E = Z \underset{˙}{-} Q$
88	1 2 3 5 11 9 14 23 87	tgcgrcomlr	$⊢ φ \to E \underset{˙}{-} R = Q \underset{˙}{-} Z$
89	1 2 3 5 13 11 13 14 84	tgcgrcomlr	$⊢ φ \to R \underset{˙}{-} Y = Z \underset{˙}{-} Y$
90	1 2 77 5 9 11 13 23 14 13 88 89 86	trgcgr	$⊢ φ \to ⟨“ E R Y ”⟩ \sim_{𝒢} (G) ⟨“ Q Z Y ”⟩$
91	1 2 3 4 41 5 9 11 13 77 23 14 13 81 90	ragcgr	$⊢ φ \to ⟨“ Q Z Y ”⟩ \in ∟_{𝒢} (G)$
92	1 2 3 4 41 5 23 14 13 91	ragcom	$⊢ φ \to ⟨“ Y Z Q ”⟩ \in ∟_{𝒢} (G)$
93	1 2 3 4 41 5 13 14 23	israg	$⊢ φ \to (⟨“ Y Z Q ”⟩ \in ∟_{𝒢} (G) \leftrightarrow Y \underset{˙}{-} Q = Y \underset{˙}{-} {pInv}_{𝒢} (G) (Z) (Q))$
94	92 93	mpbid	$⊢ φ \to Y \underset{˙}{-} Q = Y \underset{˙}{-} {pInv}_{𝒢} (G) (Z) (Q)$
95	1 2 3 5 13 23 13 54 94	tgcgrcomlr	$⊢ φ \to Q \underset{˙}{-} Y = {pInv}_{𝒢} (G) (Z) (Q) \underset{˙}{-} Y$
96	27	eqcomd	$⊢ φ \to Y \underset{˙}{-} C = Y \underset{˙}{-} D$
97	1 2 3 4 41 5 14 53 23	mircgr	$⊢ φ \to Z \underset{˙}{-} {pInv}_{𝒢} (G) (Z) (Q) = Z \underset{˙}{-} Q$
98	97	eqcomd	$⊢ φ \to Z \underset{˙}{-} Q = Z \underset{˙}{-} {pInv}_{𝒢} (G) (Z) (Q)$
99	1 2 3 5 14 23 14 54 98	tgcgrcomlr	$⊢ φ \to Q \underset{˙}{-} Z = {pInv}_{𝒢} (G) (Z) (Q) \underset{˙}{-} Z$
100		eqidd	$⊢ φ \to Y \underset{˙}{-} Z = Y \underset{˙}{-} Z$
101	1 2 3 5 23 13 7 54 13 15 14 14 63 76 26 95 96 99 100	axtg5seg	$⊢ φ \to C \underset{˙}{-} Z = D \underset{˙}{-} Z$
102	1 2 3 5 7 14 15 14 101	tgcgrcomlr	$⊢ φ \to Z \underset{˙}{-} C = Z \underset{˙}{-} D$
103	28	oveq2d	$⊢ φ \to Z \underset{˙}{-} D = Z \underset{˙}{-} {pInv}_{𝒢} (G) (X) (C)$
104	102 103	eqtrd	$⊢ φ \to Z \underset{˙}{-} C = Z \underset{˙}{-} {pInv}_{𝒢} (G) (X) (C)$
105	1 2 3 4 41 5 14 12 7	israg	$⊢ φ \to (⟨“ Z X C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow Z \underset{˙}{-} C = Z \underset{˙}{-} {pInv}_{𝒢} (G) (X) (C))$
106	104 105	mpbird	$⊢ φ \to ⟨“ Z X C ”⟩ \in ∟_{𝒢} (G)$
107	106	adantr	$⊢ (φ \land Y = X) \to ⟨“ Z X C ”⟩ \in ∟_{𝒢} (G)$
108	71	necomd	$⊢ φ \to Y \neq R$
109	1 2 3 5 13 11 13 14 84 108	tgcgrneq	$⊢ φ \to Y \neq Z$
110	109	necomd	$⊢ φ \to Z \neq Y$
111	110	adantr	$⊢ (φ \land Y = X) \to Z \neq Y$
112	111 48	neeqtrd	$⊢ (φ \land Y = X) \to Z \neq X$
113	19	eqcomd	$⊢ φ \to E \underset{˙}{-} C = E \underset{˙}{-} Y$
114	113	adantr	$⊢ (φ \land Y = X) \to E \underset{˙}{-} C = E \underset{˙}{-} Y$
115	60	adantr	$⊢ (φ \land Y = X) \to E \neq C$
116	1 2 3 42 43 46 43 44 114 115	tgcgrneq	$⊢ (φ \land Y = X) \to E \neq Y$
117	116	necomd	$⊢ (φ \land Y = X) \to Y \neq E$
118	1 2 3 5 9 7 9 13 113 60	tgcgrneq	$⊢ φ \to E \neq Y$
119	1 3 4 5 9 13 14 118 21	btwnlng3	$⊢ φ \to Z \in (E L Y)$
120	119	adantr	$⊢ (φ \land Y = X) \to Z \in (E L Y)$
121	1 3 4 42 44 43 52 117 120	lncom	$⊢ (φ \land Y = X) \to Z \in (Y L E)$
122	48	oveq1d	$⊢ (φ \land Y = X) \to Y L E = X L E$
123	121 122	eleqtrd	$⊢ (φ \land Y = X) \to Z \in (X L E)$
124	123	orcd	$⊢ (φ \land Y = X) \to (Z \in (X L E) \lor X = E)$
125	1 2 3 4 41 42 52 51 46 43 107 112 124	ragcol	$⊢ (φ \land Y = X) \to ⟨“ E X C ”⟩ \in ∟_{𝒢} (G)$
126	1 2 3 4 41 42 43 51 46 125	ragcom	$⊢ (φ \land Y = X) \to ⟨“ C X E ”⟩ \in ∟_{𝒢} (G)$
127	50 126	eqeltrd	$⊢ (φ \land Y = X) \to ⟨“ C Y E ”⟩ \in ∟_{𝒢} (G)$
128	66	adantr	$⊢ (φ \land Y = X) \to C \neq Y$
129	1 2 3 5 7 11 13 74	tgbtwncom	$⊢ φ \to R \in (Y I C)$
130	1 4 3 5 13 11 7 129	btwncolg3	$⊢ φ \to (C \in (Y L R) \lor Y = R)$
131	130	adantr	$⊢ (φ \land Y = X) \to (C \in (Y L R) \lor Y = R)$
132	1 2 3 4 41 42 46 44 43 45 127 128 131	ragcol	$⊢ (φ \land Y = X) \to ⟨“ R Y E ”⟩ \in ∟_{𝒢} (G)$
133	1 2 3 4 41 42 45 44 43 132	ragcom	$⊢ (φ \land Y = X) \to ⟨“ E Y R ”⟩ \in ∟_{𝒢} (G)$
134	81	adantr	$⊢ (φ \land Y = X) \to ⟨“ E R Y ”⟩ \in ∟_{𝒢} (G)$
135	1 2 3 4 41 42 43 44 45 133 134	ragflat	$⊢ (φ \land Y = X) \to Y = R$
136	108	adantr	$⊢ (φ \land Y = X) \to Y \neq R$
137	136	neneqd	$⊢ (φ \land Y = X) \to \neg Y = R$
138	135 137	pm2.65da	$⊢ φ \to \neg Y = X$
139	138	neqned	$⊢ φ \to Y \neq X$
140	28	oveq2d	$⊢ φ \to Y \underset{˙}{-} D = Y \underset{˙}{-} {pInv}_{𝒢} (G) (X) (C)$
141	96 140	eqtrd	$⊢ φ \to Y \underset{˙}{-} C = Y \underset{˙}{-} {pInv}_{𝒢} (G) (X) (C)$
142	1 2 3 4 41 5 13 12 7	israg	$⊢ φ \to (⟨“ Y X C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow Y \underset{˙}{-} C = Y \underset{˙}{-} {pInv}_{𝒢} (G) (X) (C))$
143	141 142	mpbird	$⊢ φ \to ⟨“ Y X C ”⟩ \in ∟_{𝒢} (G)$
144	1 2 3 4 41 5 13 12 7 143	ragcom	$⊢ φ \to ⟨“ C X Y ”⟩ \in ∟_{𝒢} (G)$
145	1 2 3 4 5 33 6 35 36 40 32 139 144	ragperp	$⊢ φ \to (C L X) ⟂_{𝒢} (G) A$

Metamath Proof Explorer

Theorem footexlem2

Proof