Theorem mideulem2 28743

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

Hypotheses

Ref	Expression
colperpex.p	⊢ 𝑃 = (Base‘𝐺)
colperpex.d	⊢ − = (dist‘𝐺)
colperpex.i	⊢ 𝐼 = (Itv‘𝐺)
colperpex.l	⊢ 𝐿 = (LineG‘𝐺)
colperpex.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
mideu.s	⊢ 𝑆 = (pInvG‘𝐺)
mideu.1	⊢ (𝜑 → 𝐴 ∈ 𝑃)
mideu.2	⊢ (𝜑 → 𝐵 ∈ 𝑃)
mideulem.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
mideulem.2	⊢ (𝜑 → 𝑄 ∈ 𝑃)
mideulem.3	⊢ (𝜑 → 𝑂 ∈ 𝑃)
mideulem.4	⊢ (𝜑 → 𝑇 ∈ 𝑃)
mideulem.5	⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
mideulem.6	⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
mideulem.7	⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵))
mideulem.8	⊢ (𝜑 → 𝑇 ∈ (𝑄𝐼𝑂))
opphllem.1	⊢ (𝜑 → 𝑅 ∈ 𝑃)
opphllem.2	⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))
opphllem.3	⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))
mideulem2.1	⊢ (𝜑 → 𝑋 ∈ 𝑃)
mideulem2.2	⊢ (𝜑 → 𝑋 ∈ (𝑇𝐼𝐵))
mideulem2.3	⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂))
mideulem2.4	⊢ (𝜑 → 𝑍 ∈ 𝑃)
mideulem2.5	⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
mideulem2.6	⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅))
mideulem2.7	⊢ (𝜑 → 𝑀 ∈ 𝑃)
mideulem2.8	⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍))

Assertion

Ref	Expression
mideulem2	⊢ (𝜑 → 𝐵 = 𝑀)

Proof of Theorem mideulem2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7440	. . 3 ⊢ (𝑦 = 𝐵 → (𝑅𝐿𝑦) = (𝑅𝐿𝐵))
2	1	breq1d 5152	. 2 ⊢ (𝑦 = 𝐵 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵)))
3		oveq2 7440	. . 3 ⊢ (𝑦 = 𝑀 → (𝑅𝐿𝑦) = (𝑅𝐿𝑀))
4	3	breq1d 5152	. 2 ⊢ (𝑦 = 𝑀 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝑀)(⟂G‘𝐺)(𝐴𝐿𝐵)))
5		colperpex.p	. . 3 ⊢ 𝑃 = (Base‘𝐺)
6		colperpex.d	. . 3 ⊢ − = (dist‘𝐺)
7		colperpex.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
8		colperpex.l	. . 3 ⊢ 𝐿 = (LineG‘𝐺)
9		colperpex.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
10		mideu.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
11		mideu.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
12		mideulem.1	. . . 4 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
13	5, 7, 8, 9, 10, 11, 12	tgelrnln 28639	. . 3 ⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
14		opphllem.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
15	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ≠ 𝐵)
16	15	neneqd 2944	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝐴 = 𝐵)
17		mideulem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ 𝑃)
18		opphllem.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))
19		mideulem.6	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
20	8, 9, 19	perpln2 28720	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴𝐿𝑂) ∈ ran 𝐿)
21	5, 7, 8, 9, 10, 17, 20	tglnne 28637	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ 𝑂)
22	5, 6, 7, 9, 10, 17, 11, 14, 18, 21	tgcgrneq 28492	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ≠ 𝑅)
23	22	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ≠ 𝑅)
24	23	necomd 2995	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ≠ 𝐵)
25	24	neneqd 2944	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝑅 = 𝐵)
26	16, 25	jca 511	. . . 4 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
27		mideu.s	. . . . . 6 ⊢ 𝑆 = (pInvG‘𝐺)
28	9	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
29	10	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃)
30	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃)
31	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ∈ 𝑃)
32		mideulem.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
33		mideulem.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
34	8, 9, 33	perpln2 28720	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄𝐿𝐵) ∈ ran 𝐿)
35	5, 7, 8, 9, 32, 11, 34	tglnne 28637	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ≠ 𝐵)
36	5, 7, 8, 9, 32, 11, 35	tglinerflx2 28643	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (𝑄𝐿𝐵))
37	5, 6, 7, 8, 9, 13, 34, 33	perpcom 28722	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
38	5, 7, 8, 9, 10, 11, 12	tglinecom 28644	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
39	37, 38	breqtrd 5168	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐵𝐿𝐴))
40	5, 6, 7, 8, 9, 32, 11, 36, 10, 39	perprag 28735	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑄𝐵𝐴”⟩ ∈ (∟G‘𝐺))
41		opphllem.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))
42	5, 8, 7, 9, 11, 14, 32, 41	btwncolg3 28566	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 ∈ (𝐵𝐿𝑅) ∨ 𝐵 = 𝑅))
43	5, 6, 7, 8, 27, 9, 32, 11, 10, 14, 40, 35, 42	ragcol 28708	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑅𝐵𝐴”⟩ ∈ (∟G‘𝐺))
44	5, 6, 7, 8, 27, 9, 14, 11, 10, 43	ragcom 28707	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐴𝐵𝑅”⟩ ∈ (∟G‘𝐺))
45	44	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ⟨“𝐴𝐵𝑅”⟩ ∈ (∟G‘𝐺))
46		animorrl 982	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
47	5, 6, 7, 8, 27, 28, 29, 30, 31, 45, 46	ragflat3 28715	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝐴 = 𝐵 ∨ 𝑅 = 𝐵))
48		oran 991	. . . . 5 ⊢ ((𝐴 = 𝐵 ∨ 𝑅 = 𝐵) ↔ ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
49	47, 48	sylib 218	. . . 4 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
50	26, 49	pm2.65da 816	. . 3 ⊢ (𝜑 → ¬ 𝑅 ∈ (𝐴𝐿𝐵))
51	5, 6, 7, 8, 9, 13, 14, 50	foot 28731	. 2 ⊢ (𝜑 → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵))
52	5, 7, 8, 9, 10, 11, 12	tglinerflx2 28643	. 2 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐿𝐵))
53		mideulem2.1	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
54	12	neneqd 2944	. . . . 5 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
55		oveq2 7440	. . . . . . 7 ⊢ (𝑦 = 𝐴 → (𝑅𝐿𝑦) = (𝑅𝐿𝐴))
56	55	breq1d 5152	. . . . . 6 ⊢ (𝑦 = 𝐴 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵)))
57	51	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵))
58	5, 7, 8, 9, 10, 11, 12	tglinerflx1 28642	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐿𝐵))
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐿𝐵))
60	52	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐵 ∈ (𝐴𝐿𝐵))
61	9	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
62	14	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ∈ 𝑃)
63	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃)
64	50, 54	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ 𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
65		pm4.56 990	. . . . . . . . . . . 12 ⊢ ((¬ 𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵) ↔ ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
66	64, 65	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
67	5, 7, 8, 9, 14, 10, 11, 66	ncolne1 28634	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ≠ 𝐴)
68	67	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝐴)
69	5, 7, 8, 61, 62, 63, 68	tglinecom 28644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑅))
70	68	necomd 2995	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ≠ 𝑅)
71	17	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ 𝑃)
72	21	necomd 2995	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ≠ 𝐴)
73	72	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝐴)
74	53	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃)
75		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴)
76	75, 70	eqnetrd 3007	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ≠ 𝑅)
77		mideulem2.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂))
78	5, 6, 7, 9, 14, 53, 17, 77	tgbtwncom 28497	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ (𝑂𝐼𝑅))
79		mideulem.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ 𝑃)
80		mideulem.7	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ (𝐴𝐿𝐵))
81		mideulem2.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ (𝑇𝐼𝐵))
82	5, 7, 8, 9, 79, 10, 11, 53, 80, 81	coltr3 28657	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐿𝐵))
83	12	necomd 2995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
84	83	neneqd 2944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
85	84	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝐵 = 𝐴)
86	72	neneqd 2944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 𝑂 = 𝐴)
87	86	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝑂 = 𝐴)
88	85, 87	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
89	9	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐺 ∈ TarskiG)
90	11	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐵 ∈ 𝑃)
91	10	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐴 ∈ 𝑃)
92	17	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂 ∈ 𝑃)
93	5, 7, 8, 9, 11, 10, 83	tglinerflx2 28643	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐴))
94	38, 19	eqbrtrrd 5166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝑂))
95	5, 6, 7, 8, 9, 11, 10, 93, 17, 94	perprag 28735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
96	95	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
97		animorrl 982	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝑂 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
98	5, 6, 7, 8, 27, 89, 90, 91, 92, 96, 97	ragflat3 28715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝐵 = 𝐴 ∨ 𝑂 = 𝐴))
99		oran 991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = 𝐴 ∨ 𝑂 = 𝐴) ↔ ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
100	98, 99	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
101	88, 100	pm2.65da 816	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
102	101, 38	neleqtrrd 2863	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
103		nelne2 3039	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑂 ∈ (𝐴𝐿𝐵)) → 𝑋 ≠ 𝑂)
104	82, 102, 103	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ≠ 𝑂)
105	5, 6, 7, 9, 17, 53, 14, 78, 104	tgbtwnne 28499	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑂 ≠ 𝑅)
106	105	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝑅)
107	106	necomd 2995	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝑂)
108	77	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐼𝑂))
109	5, 7, 8, 61, 62, 71, 74, 107, 108	btwnlng1 28628	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐿𝑂))
110	5, 7, 8, 61, 74, 62, 71, 76, 109, 107	lnrot2 28633	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝑋𝐿𝑅))
111	75	oveq1d 7447	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑋𝐿𝑅) = (𝐴𝐿𝑅))
112	110, 111	eleqtrd 2842	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝐴𝐿𝑅))
113	5, 7, 8, 61, 63, 62, 70, 71, 73, 112	tglineelsb2 28641	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑅) = (𝐴𝐿𝑂))
114	69, 113	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑂))
115	5, 6, 7, 8, 9, 13, 20, 19	perpcom 28722	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵))
116	115	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵))
117	114, 116	eqbrtrd 5164	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵))
118	13	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵) ∈ ran 𝐿)
119	22	necomd 2995	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ 𝐵)
120	5, 7, 8, 9, 14, 11, 119	tgelrnln 28639	. . . . . . . 8 ⊢ (𝜑 → (𝑅𝐿𝐵) ∈ ran 𝐿)
121	120	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵) ∈ ran 𝐿)
122	5, 7, 8, 9, 14, 11, 119	tglinerflx2 28643	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐿𝐵))
123	52, 122	elind 4199	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝐵)))
124	5, 7, 8, 9, 14, 11, 119	tglinerflx1 28642	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝐵))
125	5, 6, 7, 8, 9, 13, 120, 123, 58, 124, 12, 119, 44	ragperp 28726	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵))
126	125	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵))
127	5, 6, 7, 8, 61, 118, 121, 126	perpcom 28722	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
128	56, 2, 57, 59, 60, 117, 127	reu2eqd 3741	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝐵)
129	54, 128	mtand 815	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐴)
130	129	neqned 2946	. . 3 ⊢ (𝜑 → 𝑋 ≠ 𝐴)
131		mideulem2.7	. . 3 ⊢ (𝜑 → 𝑀 ∈ 𝑃)
132	130	necomd 2995	. . . 4 ⊢ (𝜑 → 𝐴 ≠ 𝑋)
133		eqid 2736	. . . . 5 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
134		eqid 2736	. . . . 5 ⊢ (𝑆‘𝑀) = (𝑆‘𝑀)
135	5, 6, 7, 8, 27, 9, 10, 133, 17	mircl 28670	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃)
136		mideulem2.4	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
137		mideulem2.5	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
138	82	orcd 873	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
139	5, 8, 7, 9, 10, 11, 53, 138	colcom 28567	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
140	5, 8, 7, 9, 11, 10, 53, 139	colrot1 28568	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
141	5, 6, 7, 8, 27, 9, 11, 10, 17, 53, 95, 83, 140	ragcol 28708	. . . . . 6 ⊢ (𝜑 → ⟨“𝑋𝐴𝑂”⟩ ∈ (∟G‘𝐺))
142	5, 6, 7, 8, 27, 9, 53, 10, 17	israg 28706	. . . . . 6 ⊢ (𝜑 → (⟨“𝑋𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂))))
143	141, 142	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
144		mideulem2.6	. . . . . 6 ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅))
145	144	eqcomd 2742	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑅) = (𝑋 − 𝑍))
146		eqidd 2737	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑂) = ((𝑆‘𝐴)‘𝑂))
147		mideulem2.8	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍))
148	147	eqcomd 2742	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝑀)‘𝑍) = 𝑅)
149	5, 6, 7, 8, 27, 9, 131, 134, 136, 148	mircom 28672	. . . . . 6 ⊢ (𝜑 → ((𝑆‘𝑀)‘𝑅) = 𝑍)
150	149	eqcomd 2742	. . . . 5 ⊢ (𝜑 → 𝑍 = ((𝑆‘𝑀)‘𝑅))
151	5, 6, 7, 8, 27, 9, 133, 134, 17, 135, 53, 14, 136, 10, 131, 78, 137, 143, 145, 146, 150	krippen 28700	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐼𝑀))
152	5, 7, 8, 9, 10, 53, 131, 132, 151	btwnlng3 28630	. . 3 ⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝑋))
153	5, 7, 8, 9, 10, 11, 12, 53, 130, 82, 131, 152	tglineeltr 28640	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝐵))
154	5, 6, 7, 8, 9, 13, 120, 125	perpcom 28722	. 2 ⊢ (𝜑 → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
155		nelne2 3039	. . . . . 6 ⊢ ((𝑀 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑀 ≠ 𝑅)
156	153, 50, 155	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝑅)
157	156	necomd 2995	. . . 4 ⊢ (𝜑 → 𝑅 ≠ 𝑀)
158	5, 7, 8, 9, 14, 131, 157	tgelrnln 28639	. . 3 ⊢ (𝜑 → (𝑅𝐿𝑀) ∈ ran 𝐿)
159	5, 7, 8, 9, 14, 131, 157	tglinerflx2 28643	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (𝑅𝐿𝑀))
160	153, 159	elind 4199	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝑀)))
161	5, 7, 8, 9, 14, 131, 157	tglinerflx1 28642	. . . 4 ⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝑀))
162		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝑋)
163	9	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐺 ∈ TarskiG)
164	131	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ 𝑃)
165	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐴 ∈ 𝑃)
166	17	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑂 ∈ 𝑃)
167	135	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃)
168	143	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
169	162	oveq1d 7447	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑂) = (𝑋 − 𝑂))
170	162	oveq1d 7447	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
171	168, 169, 170	3eqtr4rd 2787	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑀 − 𝑂))
172	136	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ∈ 𝑃)
173	14	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ∈ 𝑃)
174	147	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 = ((𝑆‘𝑀)‘𝑍))
175	174	oveq2d 7448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − ((𝑆‘𝑀)‘𝑍)))
176	5, 6, 7, 8, 27, 163, 164, 134, 172	mircgr 28666	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝑀)‘𝑍)) = (𝑀 − 𝑍))
177	175, 176	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − 𝑍))
178	5, 6, 7, 163, 164, 173, 164, 172, 177	tgcgrcomlr 28489	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑅 − 𝑀) = (𝑍 − 𝑀))
179	82	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝐴𝐿𝐵))
180	162, 179	eqeltrd 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝐴𝐿𝐵))
181	50	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ¬ 𝑅 ∈ (𝐴𝐿𝐵))
182	180, 181, 155	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ≠ 𝑅)
183	182	necomd 2995	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ≠ 𝑀)
184	5, 6, 7, 163, 173, 164, 172, 164, 178, 183	tgcgrneq 28492	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ≠ 𝑀)
185	5, 6, 7, 8, 27, 9, 131, 134, 136	mirbtwn 28667	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (((𝑆‘𝑀)‘𝑍)𝐼𝑍))
186	147	oveq1d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅𝐼𝑍) = (((𝑆‘𝑀)‘𝑍)𝐼𝑍))
187	185, 186	eleqtrrd 2843	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝑅𝐼𝑍))
188	187	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑍))
189	5, 6, 7, 163, 173, 164, 172, 188	tgbtwncom 28497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼𝑅))
190	137	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
191	162, 190	eqeltrd 2840	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
192	5, 6, 7, 163, 167, 164, 172, 191	tgbtwncom 28497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼((𝑆‘𝐴)‘𝑂)))
193	77	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝑅𝐼𝑂))
194	162, 193	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑂))
195	5, 7, 163, 172, 164, 173, 167, 166, 184, 183, 189, 192, 194	tgbtwnconn22 28588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑂))
196	5, 6, 7, 8, 27, 163, 164, 134, 166, 167, 171, 195	ismir 28668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) = ((𝑆‘𝑀)‘𝑂))
197	196	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝑀)‘𝑂) = ((𝑆‘𝐴)‘𝑂))
198	5, 6, 7, 8, 27, 163, 164, 165, 166, 197	miduniq1 28695	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝐴)
199	162, 198	eqtr3d 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 = 𝐴)
200	129, 199	mtand 815	. . . . . 6 ⊢ (𝜑 → ¬ 𝑀 = 𝑋)
201	200	neqned 2946	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝑋)
202	201	necomd 2995	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑀)
203	149	oveq2d 7448	. . . . . 6 ⊢ (𝜑 → (𝑋 − ((𝑆‘𝑀)‘𝑅)) = (𝑋 − 𝑍))
204	203, 144	eqtr2d 2777	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅)))
205	5, 6, 7, 8, 27, 9, 53, 131, 14	israg 28706	. . . . 5 ⊢ (𝜑 → (⟨“𝑋𝑀𝑅”⟩ ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅))))
206	204, 205	mpbird 257	. . . 4 ⊢ (𝜑 → ⟨“𝑋𝑀𝑅”⟩ ∈ (∟G‘𝐺))
207	5, 6, 7, 8, 9, 13, 158, 160, 82, 161, 202, 157, 206	ragperp 28726	. . 3 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝑀))
208	5, 6, 7, 8, 9, 13, 158, 207	perpcom 28722	. 2 ⊢ (𝜑 → (𝑅𝐿𝑀)(⟂G‘𝐺)(𝐴𝐿𝐵))
209	2, 4, 51, 52, 153, 154, 208	reu2eqd 3741	1 ⊢ (𝜑 → 𝐵 = 𝑀)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1539   ∈ wcel 2107   ≠ wne 2939  ∃!wreu 3377   class class class wbr 5142  ran crn 5685  ‘cfv 6560  (class class class)co 7432  ⟨“cs3 14882  Basecbs 17248  distcds 17307  TarskiGcstrkg 28436  Itvcitv 28442  LineGclng 28443  pInvGcmir 28661  ∟Gcrag 28702  ⟂Gcperpg 28704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-oadd 8511  df-er 8746  df-map 8869  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-dju 9942  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-2 12330  df-3 12331  df-n0 12529  df-xnn0 12602  df-z 12616  df-uz 12880  df-fz 13549  df-fzo 13696  df-hash 14371  df-word 14554  df-concat 14610  df-s1 14635  df-s2 14888  df-s3 14889  df-trkgc 28457  df-trkgb 28458  df-trkgcb 28459  df-trkg 28462  df-cgrg 28520  df-leg 28592  df-mir 28662  df-rag 28703  df-perpg 28705

This theorem is referenced by:  opphllem  28744