mideulem2

Description: Lemma for opphllem , which is itself used for mideu . (Contributed by Thierry Arnoux, 19-Feb-2020)

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
	mideu.1	$⊢ φ \to A \in P$
	mideu.2	$⊢ φ \to B \in P$
	mideulem.1	$⊢ φ \to A \neq B$
	mideulem.2	$⊢ φ \to Q \in P$
	mideulem.3	$⊢ φ \to O \in P$
	mideulem.4	$⊢ φ \to T \in P$
	mideulem.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (Q L B)$
	mideulem.6	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (A L O)$
	mideulem.7	$⊢ φ \to T \in (A L B)$
	mideulem.8	$⊢ φ \to T \in (Q I O)$
	opphllem.1	$⊢ φ \to R \in P$
	opphllem.2	$⊢ φ \to R \in (B I Q)$
	opphllem.3	$⊢ φ \to A \underset{˙}{-} O = B \underset{˙}{-} R$
	mideulem2.1	$⊢ φ \to X \in P$
	mideulem2.2	$⊢ φ \to X \in (T I B)$
	mideulem2.3	$⊢ φ \to X \in (R I O)$
	mideulem2.4	$⊢ φ \to Z \in P$
	mideulem2.5	$⊢ φ \to X \in (S (A) (O) I Z)$
	mideulem2.6	$⊢ φ \to X \underset{˙}{-} Z = X \underset{˙}{-} R$
	mideulem2.7	$⊢ φ \to M \in P$
	mideulem2.8	$⊢ φ \to R = S (M) (Z)$
Assertion	mideulem2	$⊢ φ \to B = M$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
7		mideu.1	$⊢ φ \to A \in P$
8		mideu.2	$⊢ φ \to B \in P$
9		mideulem.1	$⊢ φ \to A \neq B$
10		mideulem.2	$⊢ φ \to Q \in P$
11		mideulem.3	$⊢ φ \to O \in P$
12		mideulem.4	$⊢ φ \to T \in P$
13		mideulem.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (Q L B)$
14		mideulem.6	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (A L O)$
15		mideulem.7	$⊢ φ \to T \in (A L B)$
16		mideulem.8	$⊢ φ \to T \in (Q I O)$
17		opphllem.1	$⊢ φ \to R \in P$
18		opphllem.2	$⊢ φ \to R \in (B I Q)$
19		opphllem.3	$⊢ φ \to A \underset{˙}{-} O = B \underset{˙}{-} R$
20		mideulem2.1	$⊢ φ \to X \in P$
21		mideulem2.2	$⊢ φ \to X \in (T I B)$
22		mideulem2.3	$⊢ φ \to X \in (R I O)$
23		mideulem2.4	$⊢ φ \to Z \in P$
24		mideulem2.5	$⊢ φ \to X \in (S (A) (O) I Z)$
25		mideulem2.6	$⊢ φ \to X \underset{˙}{-} Z = X \underset{˙}{-} R$
26		mideulem2.7	$⊢ φ \to M \in P$
27		mideulem2.8	$⊢ φ \to R = S (M) (Z)$
28		oveq2	$⊢ y = B \to R L y = R L B$
29	28	breq1d	$⊢ y = B \to ((R L y) ⟂_{𝒢} (G) (A L B) \leftrightarrow (R L B) ⟂_{𝒢} (G) (A L B))$
30		oveq2	$⊢ y = M \to R L y = R L M$
31	30	breq1d	$⊢ y = M \to ((R L y) ⟂_{𝒢} (G) (A L B) \leftrightarrow (R L M) ⟂_{𝒢} (G) (A L B))$
32	1 3 4 5 7 8 9	tgelrnln	$⊢ φ \to A L B \in ran L$
33	9	adantr	$⊢ (φ \land R \in (A L B)) \to A \neq B$
34	33	neneqd	$⊢ (φ \land R \in (A L B)) \to \neg A = B$
35	4 5 14	perpln2	$⊢ φ \to A L O \in ran L$
36	1 3 4 5 7 11 35	tglnne	$⊢ φ \to A \neq O$
37	1 2 3 5 7 11 8 17 19 36	tgcgrneq	$⊢ φ \to B \neq R$
38	37	adantr	$⊢ (φ \land R \in (A L B)) \to B \neq R$
39	38	necomd	$⊢ (φ \land R \in (A L B)) \to R \neq B$
40	39	neneqd	$⊢ (φ \land R \in (A L B)) \to \neg R = B$
41	34 40	jca	$⊢ (φ \land R \in (A L B)) \to (\neg A = B \land \neg R = B)$
42	5	adantr	$⊢ (φ \land R \in (A L B)) \to G \in 𝒢_{Tarski}$
43	7	adantr	$⊢ (φ \land R \in (A L B)) \to A \in P$
44	8	adantr	$⊢ (φ \land R \in (A L B)) \to B \in P$
45	17	adantr	$⊢ (φ \land R \in (A L B)) \to R \in P$
46	4 5 13	perpln2	$⊢ φ \to Q L B \in ran L$
47	1 3 4 5 10 8 46	tglnne	$⊢ φ \to Q \neq B$
48	1 3 4 5 10 8 47	tglinerflx2	$⊢ φ \to B \in (Q L B)$
49	1 2 3 4 5 32 46 13	perpcom	$⊢ φ \to (Q L B) ⟂_{𝒢} (G) (A L B)$
50	1 3 4 5 7 8 9	tglinecom	$⊢ φ \to A L B = B L A$
51	49 50	breqtrd	$⊢ φ \to (Q L B) ⟂_{𝒢} (G) (B L A)$
52	1 2 3 4 5 10 8 48 7 51	perprag	$⊢ φ \to ⟨“ Q B A ”⟩ \in ∟_{𝒢} (G)$
53	1 4 3 5 8 17 10 18	btwncolg3	$⊢ φ \to (Q \in (B L R) \lor B = R)$
54	1 2 3 4 6 5 10 8 7 17 52 47 53	ragcol	$⊢ φ \to ⟨“ R B A ”⟩ \in ∟_{𝒢} (G)$
55	1 2 3 4 6 5 17 8 7 54	ragcom	$⊢ φ \to ⟨“ A B R ”⟩ \in ∟_{𝒢} (G)$
56	55	adantr	$⊢ (φ \land R \in (A L B)) \to ⟨“ A B R ”⟩ \in ∟_{𝒢} (G)$
57		animorrl	$⊢ (φ \land R \in (A L B)) \to (R \in (A L B) \lor A = B)$
58	1 2 3 4 6 42 43 44 45 56 57	ragflat3	$⊢ (φ \land R \in (A L B)) \to (A = B \lor R = B)$
59		oran	$⊢ (A = B \lor R = B) \leftrightarrow \neg (\neg A = B \land \neg R = B)$
60	58 59	sylib	$⊢ (φ \land R \in (A L B)) \to \neg (\neg A = B \land \neg R = B)$
61	41 60	pm2.65da	$⊢ φ \to \neg R \in (A L B)$
62	1 2 3 4 5 32 17 61	foot	$⊢ φ \to \exists! y \in (A L B) (R L y) ⟂_{𝒢} (G) (A L B)$
63	1 3 4 5 7 8 9	tglinerflx2	$⊢ φ \to B \in (A L B)$
64	9	neneqd	$⊢ φ \to \neg A = B$
65		oveq2	$⊢ y = A \to R L y = R L A$
66	65	breq1d	$⊢ y = A \to ((R L y) ⟂_{𝒢} (G) (A L B) \leftrightarrow (R L A) ⟂_{𝒢} (G) (A L B))$
67	62	adantr	$⊢ (φ \land X = A) \to \exists! y \in (A L B) (R L y) ⟂_{𝒢} (G) (A L B)$
68	1 3 4 5 7 8 9	tglinerflx1	$⊢ φ \to A \in (A L B)$
69	68	adantr	$⊢ (φ \land X = A) \to A \in (A L B)$
70	63	adantr	$⊢ (φ \land X = A) \to B \in (A L B)$
71	5	adantr	$⊢ (φ \land X = A) \to G \in 𝒢_{Tarski}$
72	17	adantr	$⊢ (φ \land X = A) \to R \in P$
73	7	adantr	$⊢ (φ \land X = A) \to A \in P$
74	61 64	jca	$⊢ φ \to (\neg R \in (A L B) \land \neg A = B)$
75		pm4.56	$⊢ (\neg R \in (A L B) \land \neg A = B) \leftrightarrow \neg (R \in (A L B) \lor A = B)$
76	74 75	sylib	$⊢ φ \to \neg (R \in (A L B) \lor A = B)$
77	1 3 4 5 17 7 8 76	ncolne1	$⊢ φ \to R \neq A$
78	77	adantr	$⊢ (φ \land X = A) \to R \neq A$
79	1 3 4 71 72 73 78	tglinecom	$⊢ (φ \land X = A) \to R L A = A L R$
80	78	necomd	$⊢ (φ \land X = A) \to A \neq R$
81	11	adantr	$⊢ (φ \land X = A) \to O \in P$
82	36	necomd	$⊢ φ \to O \neq A$
83	82	adantr	$⊢ (φ \land X = A) \to O \neq A$
84	20	adantr	$⊢ (φ \land X = A) \to X \in P$
85		simpr	$⊢ (φ \land X = A) \to X = A$
86	85 80	eqnetrd	$⊢ (φ \land X = A) \to X \neq R$
87	1 2 3 5 17 20 11 22	tgbtwncom	$⊢ φ \to X \in (O I R)$
88	1 3 4 5 12 7 8 20 15 21	coltr3	$⊢ φ \to X \in (A L B)$
89	9	necomd	$⊢ φ \to B \neq A$
90	89	neneqd	$⊢ φ \to \neg B = A$
91	90	adantr	$⊢ (φ \land O \in (B L A)) \to \neg B = A$
92	82	neneqd	$⊢ φ \to \neg O = A$
93	92	adantr	$⊢ (φ \land O \in (B L A)) \to \neg O = A$
94	91 93	jca	$⊢ (φ \land O \in (B L A)) \to (\neg B = A \land \neg O = A)$
95	5	adantr	$⊢ (φ \land O \in (B L A)) \to G \in 𝒢_{Tarski}$
96	8	adantr	$⊢ (φ \land O \in (B L A)) \to B \in P$
97	7	adantr	$⊢ (φ \land O \in (B L A)) \to A \in P$
98	11	adantr	$⊢ (φ \land O \in (B L A)) \to O \in P$
99	1 3 4 5 8 7 89	tglinerflx2	$⊢ φ \to A \in (B L A)$
100	50 14	eqbrtrrd	$⊢ φ \to (B L A) ⟂_{𝒢} (G) (A L O)$
101	1 2 3 4 5 8 7 99 11 100	perprag	$⊢ φ \to ⟨“ B A O ”⟩ \in ∟_{𝒢} (G)$
102	101	adantr	$⊢ (φ \land O \in (B L A)) \to ⟨“ B A O ”⟩ \in ∟_{𝒢} (G)$
103		animorrl	$⊢ (φ \land O \in (B L A)) \to (O \in (B L A) \lor B = A)$
104	1 2 3 4 6 95 96 97 98 102 103	ragflat3	$⊢ (φ \land O \in (B L A)) \to (B = A \lor O = A)$
105		oran	$⊢ (B = A \lor O = A) \leftrightarrow \neg (\neg B = A \land \neg O = A)$
106	104 105	sylib	$⊢ (φ \land O \in (B L A)) \to \neg (\neg B = A \land \neg O = A)$
107	94 106	pm2.65da	$⊢ φ \to \neg O \in (B L A)$
108	107 50	neleqtrrd	$⊢ φ \to \neg O \in (A L B)$
109		nelne2	$⊢ (X \in (A L B) \land \neg O \in (A L B)) \to X \neq O$
110	88 108 109	syl2anc	$⊢ φ \to X \neq O$
111	1 2 3 5 11 20 17 87 110	tgbtwnne	$⊢ φ \to O \neq R$
112	111	adantr	$⊢ (φ \land X = A) \to O \neq R$
113	112	necomd	$⊢ (φ \land X = A) \to R \neq O$
114	22	adantr	$⊢ (φ \land X = A) \to X \in (R I O)$
115	1 3 4 71 72 81 84 113 114	btwnlng1	$⊢ (φ \land X = A) \to X \in (R L O)$
116	1 3 4 71 84 72 81 86 115 113	lnrot2	$⊢ (φ \land X = A) \to O \in (X L R)$
117	85	oveq1d	$⊢ (φ \land X = A) \to X L R = A L R$
118	116 117	eleqtrd	$⊢ (φ \land X = A) \to O \in (A L R)$
119	1 3 4 71 73 72 80 81 83 118	tglineelsb2	$⊢ (φ \land X = A) \to A L R = A L O$
120	79 119	eqtrd	$⊢ (φ \land X = A) \to R L A = A L O$
121	1 2 3 4 5 32 35 14	perpcom	$⊢ φ \to (A L O) ⟂_{𝒢} (G) (A L B)$
122	121	adantr	$⊢ (φ \land X = A) \to (A L O) ⟂_{𝒢} (G) (A L B)$
123	120 122	eqbrtrd	$⊢ (φ \land X = A) \to (R L A) ⟂_{𝒢} (G) (A L B)$
124	32	adantr	$⊢ (φ \land X = A) \to A L B \in ran L$
125	37	necomd	$⊢ φ \to R \neq B$
126	1 3 4 5 17 8 125	tgelrnln	$⊢ φ \to R L B \in ran L$
127	126	adantr	$⊢ (φ \land X = A) \to R L B \in ran L$
128	1 3 4 5 17 8 125	tglinerflx2	$⊢ φ \to B \in (R L B)$
129	63 128	elind	$⊢ φ \to B \in ((A L B) \cap (R L B))$
130	1 3 4 5 17 8 125	tglinerflx1	$⊢ φ \to R \in (R L B)$
131	1 2 3 4 5 32 126 129 68 130 9 125 55	ragperp	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (R L B)$
132	131	adantr	$⊢ (φ \land X = A) \to (A L B) ⟂_{𝒢} (G) (R L B)$
133	1 2 3 4 71 124 127 132	perpcom	$⊢ (φ \land X = A) \to (R L B) ⟂_{𝒢} (G) (A L B)$
134	66 29 67 69 70 123 133	reu2eqd	$⊢ (φ \land X = A) \to A = B$
135	64 134	mtand	$⊢ φ \to \neg X = A$
136	135	neqned	$⊢ φ \to X \neq A$
137	136	necomd	$⊢ φ \to A \neq X$
138		eqid	$⊢ S (A) = S (A)$
139		eqid	$⊢ S (M) = S (M)$
140	1 2 3 4 6 5 7 138 11	mircl	$⊢ φ \to S (A) (O) \in P$
141	88	orcd	$⊢ φ \to (X \in (A L B) \lor A = B)$
142	1 4 3 5 7 8 20 141	colcom	$⊢ φ \to (X \in (B L A) \lor B = A)$
143	1 4 3 5 8 7 20 142	colrot1	$⊢ φ \to (B \in (A L X) \lor A = X)$
144	1 2 3 4 6 5 8 7 11 20 101 89 143	ragcol	$⊢ φ \to ⟨“ X A O ”⟩ \in ∟_{𝒢} (G)$
145	1 2 3 4 6 5 20 7 11	israg	$⊢ φ \to (⟨“ X A O ”⟩ \in ∟_{𝒢} (G) \leftrightarrow X \underset{˙}{-} O = X \underset{˙}{-} S (A) (O))$
146	144 145	mpbid	$⊢ φ \to X \underset{˙}{-} O = X \underset{˙}{-} S (A) (O)$
147	25	eqcomd	$⊢ φ \to X \underset{˙}{-} R = X \underset{˙}{-} Z$
148		eqidd	$⊢ φ \to S (A) (O) = S (A) (O)$
149	27	eqcomd	$⊢ φ \to S (M) (Z) = R$
150	1 2 3 4 6 5 26 139 23 149	mircom	$⊢ φ \to S (M) (R) = Z$
151	150	eqcomd	$⊢ φ \to Z = S (M) (R)$
152	1 2 3 4 6 5 138 139 11 140 20 17 23 7 26 87 24 146 147 148 151	krippen	$⊢ φ \to X \in (A I M)$
153	1 3 4 5 7 20 26 137 152	btwnlng3	$⊢ φ \to M \in (A L X)$
154	1 3 4 5 7 8 9 20 136 88 26 153	tglineeltr	$⊢ φ \to M \in (A L B)$
155	1 2 3 4 5 32 126 131	perpcom	$⊢ φ \to (R L B) ⟂_{𝒢} (G) (A L B)$
156		nelne2	$⊢ (M \in (A L B) \land \neg R \in (A L B)) \to M \neq R$
157	154 61 156	syl2anc	$⊢ φ \to M \neq R$
158	157	necomd	$⊢ φ \to R \neq M$
159	1 3 4 5 17 26 158	tgelrnln	$⊢ φ \to R L M \in ran L$
160	1 3 4 5 17 26 158	tglinerflx2	$⊢ φ \to M \in (R L M)$
161	154 160	elind	$⊢ φ \to M \in ((A L B) \cap (R L M))$
162	1 3 4 5 17 26 158	tglinerflx1	$⊢ φ \to R \in (R L M)$
163		simpr	$⊢ (φ \land M = X) \to M = X$
164	5	adantr	$⊢ (φ \land M = X) \to G \in 𝒢_{Tarski}$
165	26	adantr	$⊢ (φ \land M = X) \to M \in P$
166	7	adantr	$⊢ (φ \land M = X) \to A \in P$
167	11	adantr	$⊢ (φ \land M = X) \to O \in P$
168	140	adantr	$⊢ (φ \land M = X) \to S (A) (O) \in P$
169	146	adantr	$⊢ (φ \land M = X) \to X \underset{˙}{-} O = X \underset{˙}{-} S (A) (O)$
170	163	oveq1d	$⊢ (φ \land M = X) \to M \underset{˙}{-} O = X \underset{˙}{-} O$
171	163	oveq1d	$⊢ (φ \land M = X) \to M \underset{˙}{-} S (A) (O) = X \underset{˙}{-} S (A) (O)$
172	169 170 171	3eqtr4rd	$⊢ (φ \land M = X) \to M \underset{˙}{-} S (A) (O) = M \underset{˙}{-} O$
173	23	adantr	$⊢ (φ \land M = X) \to Z \in P$
174	17	adantr	$⊢ (φ \land M = X) \to R \in P$
175	27	adantr	$⊢ (φ \land M = X) \to R = S (M) (Z)$
176	175	oveq2d	$⊢ (φ \land M = X) \to M \underset{˙}{-} R = M \underset{˙}{-} S (M) (Z)$
177	1 2 3 4 6 164 165 139 173	mircgr	$⊢ (φ \land M = X) \to M \underset{˙}{-} S (M) (Z) = M \underset{˙}{-} Z$
178	176 177	eqtrd	$⊢ (φ \land M = X) \to M \underset{˙}{-} R = M \underset{˙}{-} Z$
179	1 2 3 164 165 174 165 173 178	tgcgrcomlr	$⊢ (φ \land M = X) \to R \underset{˙}{-} M = Z \underset{˙}{-} M$
180	88	adantr	$⊢ (φ \land M = X) \to X \in (A L B)$
181	163 180	eqeltrd	$⊢ (φ \land M = X) \to M \in (A L B)$
182	61	adantr	$⊢ (φ \land M = X) \to \neg R \in (A L B)$
183	181 182 156	syl2anc	$⊢ (φ \land M = X) \to M \neq R$
184	183	necomd	$⊢ (φ \land M = X) \to R \neq M$
185	1 2 3 164 174 165 173 165 179 184	tgcgrneq	$⊢ (φ \land M = X) \to Z \neq M$
186	1 2 3 4 6 5 26 139 23	mirbtwn	$⊢ φ \to M \in (S (M) (Z) I Z)$
187	27	oveq1d	$⊢ φ \to R I Z = S (M) (Z) I Z$
188	186 187	eleqtrrd	$⊢ φ \to M \in (R I Z)$
189	188	adantr	$⊢ (φ \land M = X) \to M \in (R I Z)$
190	1 2 3 164 174 165 173 189	tgbtwncom	$⊢ (φ \land M = X) \to M \in (Z I R)$
191	24	adantr	$⊢ (φ \land M = X) \to X \in (S (A) (O) I Z)$
192	163 191	eqeltrd	$⊢ (φ \land M = X) \to M \in (S (A) (O) I Z)$
193	1 2 3 164 168 165 173 192	tgbtwncom	$⊢ (φ \land M = X) \to M \in (Z I S (A) (O))$
194	22	adantr	$⊢ (φ \land M = X) \to X \in (R I O)$
195	163 194	eqeltrd	$⊢ (φ \land M = X) \to M \in (R I O)$
196	1 3 164 173 165 174 168 167 185 184 190 193 195	tgbtwnconn22	$⊢ (φ \land M = X) \to M \in (S (A) (O) I O)$
197	1 2 3 4 6 164 165 139 167 168 172 196	ismir	$⊢ (φ \land M = X) \to S (A) (O) = S (M) (O)$
198	197	eqcomd	$⊢ (φ \land M = X) \to S (M) (O) = S (A) (O)$
199	1 2 3 4 6 164 165 166 167 198	miduniq1	$⊢ (φ \land M = X) \to M = A$
200	163 199	eqtr3d	$⊢ (φ \land M = X) \to X = A$
201	135 200	mtand	$⊢ φ \to \neg M = X$
202	201	neqned	$⊢ φ \to M \neq X$
203	202	necomd	$⊢ φ \to X \neq M$
204	150	oveq2d	$⊢ φ \to X \underset{˙}{-} S (M) (R) = X \underset{˙}{-} Z$
205	204 25	eqtr2d	$⊢ φ \to X \underset{˙}{-} R = X \underset{˙}{-} S (M) (R)$
206	1 2 3 4 6 5 20 26 17	israg	$⊢ φ \to (⟨“ X M R ”⟩ \in ∟_{𝒢} (G) \leftrightarrow X \underset{˙}{-} R = X \underset{˙}{-} S (M) (R))$
207	205 206	mpbird	$⊢ φ \to ⟨“ X M R ”⟩ \in ∟_{𝒢} (G)$
208	1 2 3 4 5 32 159 161 88 162 203 158 207	ragperp	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (R L M)$
209	1 2 3 4 5 32 159 208	perpcom	$⊢ φ \to (R L M) ⟂_{𝒢} (G) (A L B)$
210	29 31 62 63 154 155 209	reu2eqd	$⊢ φ \to B = M$

Metamath Proof Explorer

Theorem mideulem2

Proof