Theorem mideulem2 27676

Description: Lemma for opphllem 27677, which is itself used for mideu 27680. (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 7365	. . 3 ⊢ (𝑦 = 𝐵 → (𝑅𝐿𝑦) = (𝑅𝐿𝐵))
2	1	breq1d 5115	. 2 ⊢ (𝑦 = 𝐵 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵)))
3		oveq2 7365	. . 3 ⊢ (𝑦 = 𝑀 → (𝑅𝐿𝑦) = (𝑅𝐿𝑀))
4	3	breq1d 5115	. 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 27572	. . 3 ⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
14		opphllem.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
15	12	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ≠ 𝐵)
16	15	neneqd 2948	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝐴 = 𝐵)
17		mideulem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ 𝑃)
18		opphllem.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))
19		mideulem.6	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
20	8, 9, 19	perpln2 27653	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴𝐿𝑂) ∈ ran 𝐿)
21	5, 7, 8, 9, 10, 17, 20	tglnne 27570	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ 𝑂)
22	5, 6, 7, 9, 10, 17, 11, 14, 18, 21	tgcgrneq 27425	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ≠ 𝑅)
23	22	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ≠ 𝑅)
24	23	necomd 2999	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ≠ 𝐵)
25	24	neneqd 2948	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝑅 = 𝐵)
26	16, 25	jca 512	. . . 4 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
27		mideu.s	. . . . . 6 ⊢ 𝑆 = (pInvG‘𝐺)
28	9	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
29	10	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃)
30	11	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃)
31	14	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ∈ 𝑃)
32		mideulem.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
33		mideulem.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
34	8, 9, 33	perpln2 27653	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄𝐿𝐵) ∈ ran 𝐿)
35	5, 7, 8, 9, 32, 11, 34	tglnne 27570	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ≠ 𝐵)
36	5, 7, 8, 9, 32, 11, 35	tglinerflx2 27576	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (𝑄𝐿𝐵))
37	5, 6, 7, 8, 9, 13, 34, 33	perpcom 27655	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
38	5, 7, 8, 9, 10, 11, 12	tglinecom 27577	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
39	37, 38	breqtrd 5131	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐵𝐿𝐴))
40	5, 6, 7, 8, 9, 32, 11, 36, 10, 39	perprag 27668	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑄𝐵𝐴”⟩ ∈ (∟G‘𝐺))
41		opphllem.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))
42	5, 8, 7, 9, 11, 14, 32, 41	btwncolg3 27499	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 ∈ (𝐵𝐿𝑅) ∨ 𝐵 = 𝑅))
43	5, 6, 7, 8, 27, 9, 32, 11, 10, 14, 40, 35, 42	ragcol 27641	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑅𝐵𝐴”⟩ ∈ (∟G‘𝐺))
44	5, 6, 7, 8, 27, 9, 14, 11, 10, 43	ragcom 27640	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐴𝐵𝑅”⟩ ∈ (∟G‘𝐺))
45	44	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ⟨“𝐴𝐵𝑅”⟩ ∈ (∟G‘𝐺))
46		animorrl 979	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
47	5, 6, 7, 8, 27, 28, 29, 30, 31, 45, 46	ragflat3 27648	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝐴 = 𝐵 ∨ 𝑅 = 𝐵))
48		oran 988	. . . . 5 ⊢ ((𝐴 = 𝐵 ∨ 𝑅 = 𝐵) ↔ ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
49	47, 48	sylib 217	. . . 4 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
50	26, 49	pm2.65da 815	. . 3 ⊢ (𝜑 → ¬ 𝑅 ∈ (𝐴𝐿𝐵))
51	5, 6, 7, 8, 9, 13, 14, 50	foot 27664	. 2 ⊢ (𝜑 → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵))
52	5, 7, 8, 9, 10, 11, 12	tglinerflx2 27576	. 2 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐿𝐵))
53		mideulem2.1	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
54	12	neneqd 2948	. . . . 5 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
55		oveq2 7365	. . . . . . 7 ⊢ (𝑦 = 𝐴 → (𝑅𝐿𝑦) = (𝑅𝐿𝐴))
56	55	breq1d 5115	. . . . . 6 ⊢ (𝑦 = 𝐴 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵)))
57	51	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵))
58	5, 7, 8, 9, 10, 11, 12	tglinerflx1 27575	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐿𝐵))
59	58	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐿𝐵))
60	52	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐵 ∈ (𝐴𝐿𝐵))
61	9	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
62	14	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ∈ 𝑃)
63	10	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃)
64	50, 54	jca 512	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ 𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
65		pm4.56 987	. . . . . . . . . . . 12 ⊢ ((¬ 𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵) ↔ ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
66	64, 65	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
67	5, 7, 8, 9, 14, 10, 11, 66	ncolne1 27567	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ≠ 𝐴)
68	67	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝐴)
69	5, 7, 8, 61, 62, 63, 68	tglinecom 27577	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑅))
70	68	necomd 2999	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ≠ 𝑅)
71	17	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ 𝑃)
72	21	necomd 2999	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ≠ 𝐴)
73	72	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝐴)
74	53	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃)
75		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴)
76	75, 70	eqnetrd 3011	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ≠ 𝑅)
77		mideulem2.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂))
78	5, 6, 7, 9, 14, 53, 17, 77	tgbtwncom 27430	. . . . . . . . . . . . . . 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 27590	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐿𝐵))
83	12	necomd 2999	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
84	83	neneqd 2948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
85	84	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝐵 = 𝐴)
86	72	neneqd 2948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 𝑂 = 𝐴)
87	86	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝑂 = 𝐴)
88	85, 87	jca 512	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
89	9	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐺 ∈ TarskiG)
90	11	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐵 ∈ 𝑃)
91	10	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐴 ∈ 𝑃)
92	17	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂 ∈ 𝑃)
93	5, 7, 8, 9, 11, 10, 83	tglinerflx2 27576	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐴))
94	38, 19	eqbrtrrd 5129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝑂))
95	5, 6, 7, 8, 9, 11, 10, 93, 17, 94	perprag 27668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
96	95	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
97		animorrl 979	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝑂 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
98	5, 6, 7, 8, 27, 89, 90, 91, 92, 96, 97	ragflat3 27648	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝐵 = 𝐴 ∨ 𝑂 = 𝐴))
99		oran 988	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = 𝐴 ∨ 𝑂 = 𝐴) ↔ ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
100	98, 99	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
101	88, 100	pm2.65da 815	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
102	101, 38	neleqtrrd 2860	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
103		nelne2 3042	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑂 ∈ (𝐴𝐿𝐵)) → 𝑋 ≠ 𝑂)
104	82, 102, 103	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ≠ 𝑂)
105	5, 6, 7, 9, 17, 53, 14, 78, 104	tgbtwnne 27432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑂 ≠ 𝑅)
106	105	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝑅)
107	106	necomd 2999	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝑂)
108	77	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐼𝑂))
109	5, 7, 8, 61, 62, 71, 74, 107, 108	btwnlng1 27561	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐿𝑂))
110	5, 7, 8, 61, 74, 62, 71, 76, 109, 107	lnrot2 27566	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝑋𝐿𝑅))
111	75	oveq1d 7372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑋𝐿𝑅) = (𝐴𝐿𝑅))
112	110, 111	eleqtrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝐴𝐿𝑅))
113	5, 7, 8, 61, 63, 62, 70, 71, 73, 112	tglineelsb2 27574	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑅) = (𝐴𝐿𝑂))
114	69, 113	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑂))
115	5, 6, 7, 8, 9, 13, 20, 19	perpcom 27655	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵))
116	115	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵))
117	114, 116	eqbrtrd 5127	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵))
118	13	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵) ∈ ran 𝐿)
119	22	necomd 2999	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ 𝐵)
120	5, 7, 8, 9, 14, 11, 119	tgelrnln 27572	. . . . . . . 8 ⊢ (𝜑 → (𝑅𝐿𝐵) ∈ ran 𝐿)
121	120	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵) ∈ ran 𝐿)
122	5, 7, 8, 9, 14, 11, 119	tglinerflx2 27576	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐿𝐵))
123	52, 122	elind 4154	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝐵)))
124	5, 7, 8, 9, 14, 11, 119	tglinerflx1 27575	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝐵))
125	5, 6, 7, 8, 9, 13, 120, 123, 58, 124, 12, 119, 44	ragperp 27659	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵))
126	125	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵))
127	5, 6, 7, 8, 61, 118, 121, 126	perpcom 27655	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
128	56, 2, 57, 59, 60, 117, 127	reu2eqd 3694	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝐵)
129	54, 128	mtand 814	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐴)
130	129	neqned 2950	. . 3 ⊢ (𝜑 → 𝑋 ≠ 𝐴)
131		mideulem2.7	. . 3 ⊢ (𝜑 → 𝑀 ∈ 𝑃)
132	130	necomd 2999	. . . 4 ⊢ (𝜑 → 𝐴 ≠ 𝑋)
133		eqid 2736	. . . . 5 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
134		eqid 2736	. . . . 5 ⊢ (𝑆‘𝑀) = (𝑆‘𝑀)
135	5, 6, 7, 8, 27, 9, 10, 133, 17	mircl 27603	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃)
136		mideulem2.4	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
137		mideulem2.5	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
138	82	orcd 871	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
139	5, 8, 7, 9, 10, 11, 53, 138	colcom 27500	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
140	5, 8, 7, 9, 11, 10, 53, 139	colrot1 27501	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
141	5, 6, 7, 8, 27, 9, 11, 10, 17, 53, 95, 83, 140	ragcol 27641	. . . . . 6 ⊢ (𝜑 → ⟨“𝑋𝐴𝑂”⟩ ∈ (∟G‘𝐺))
142	5, 6, 7, 8, 27, 9, 53, 10, 17	israg 27639	. . . . . 6 ⊢ (𝜑 → (⟨“𝑋𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂))))
143	141, 142	mpbid 231	. . . . 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 27605	. . . . . 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 27633	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐼𝑀))
152	5, 7, 8, 9, 10, 53, 131, 132, 151	btwnlng3 27563	. . 3 ⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝑋))
153	5, 7, 8, 9, 10, 11, 12, 53, 130, 82, 131, 152	tglineeltr 27573	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝐵))
154	5, 6, 7, 8, 9, 13, 120, 125	perpcom 27655	. 2 ⊢ (𝜑 → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
155		nelne2 3042	. . . . . 6 ⊢ ((𝑀 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑀 ≠ 𝑅)
156	153, 50, 155	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝑅)
157	156	necomd 2999	. . . 4 ⊢ (𝜑 → 𝑅 ≠ 𝑀)
158	5, 7, 8, 9, 14, 131, 157	tgelrnln 27572	. . 3 ⊢ (𝜑 → (𝑅𝐿𝑀) ∈ ran 𝐿)
159	5, 7, 8, 9, 14, 131, 157	tglinerflx2 27576	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (𝑅𝐿𝑀))
160	153, 159	elind 4154	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝑀)))
161	5, 7, 8, 9, 14, 131, 157	tglinerflx1 27575	. . . 4 ⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝑀))
162		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝑋)
163	9	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐺 ∈ TarskiG)
164	131	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ 𝑃)
165	10	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐴 ∈ 𝑃)
166	17	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑂 ∈ 𝑃)
167	135	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃)
168	143	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
169	162	oveq1d 7372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑂) = (𝑋 − 𝑂))
170	162	oveq1d 7372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
171	168, 169, 170	3eqtr4rd 2787	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑀 − 𝑂))
172	136	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ∈ 𝑃)
173	14	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ∈ 𝑃)
174	147	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 = ((𝑆‘𝑀)‘𝑍))
175	174	oveq2d 7373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − ((𝑆‘𝑀)‘𝑍)))
176	5, 6, 7, 8, 27, 163, 164, 134, 172	mircgr 27599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝑀)‘𝑍)) = (𝑀 − 𝑍))
177	175, 176	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − 𝑍))
178	5, 6, 7, 163, 164, 173, 164, 172, 177	tgcgrcomlr 27422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑅 − 𝑀) = (𝑍 − 𝑀))
179	82	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝐴𝐿𝐵))
180	162, 179	eqeltrd 2838	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝐴𝐿𝐵))
181	50	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ¬ 𝑅 ∈ (𝐴𝐿𝐵))
182	180, 181, 155	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ≠ 𝑅)
183	182	necomd 2999	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ≠ 𝑀)
184	5, 6, 7, 163, 173, 164, 172, 164, 178, 183	tgcgrneq 27425	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ≠ 𝑀)
185	5, 6, 7, 8, 27, 9, 131, 134, 136	mirbtwn 27600	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (((𝑆‘𝑀)‘𝑍)𝐼𝑍))
186	147	oveq1d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅𝐼𝑍) = (((𝑆‘𝑀)‘𝑍)𝐼𝑍))
187	185, 186	eleqtrrd 2841	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝑅𝐼𝑍))
188	187	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑍))
189	5, 6, 7, 163, 173, 164, 172, 188	tgbtwncom 27430	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼𝑅))
190	137	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
191	162, 190	eqeltrd 2838	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
192	5, 6, 7, 163, 167, 164, 172, 191	tgbtwncom 27430	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼((𝑆‘𝐴)‘𝑂)))
193	77	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝑅𝐼𝑂))
194	162, 193	eqeltrd 2838	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑂))
195	5, 7, 163, 172, 164, 173, 167, 166, 184, 183, 189, 192, 194	tgbtwnconn22 27521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑂))
196	5, 6, 7, 8, 27, 163, 164, 134, 166, 167, 171, 195	ismir 27601	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) = ((𝑆‘𝑀)‘𝑂))
197	196	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝑀)‘𝑂) = ((𝑆‘𝐴)‘𝑂))
198	5, 6, 7, 8, 27, 163, 164, 165, 166, 197	miduniq1 27628	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝐴)
199	162, 198	eqtr3d 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 = 𝐴)
200	129, 199	mtand 814	. . . . . 6 ⊢ (𝜑 → ¬ 𝑀 = 𝑋)
201	200	neqned 2950	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝑋)
202	201	necomd 2999	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑀)
203	149	oveq2d 7373	. . . . . 6 ⊢ (𝜑 → (𝑋 − ((𝑆‘𝑀)‘𝑅)) = (𝑋 − 𝑍))
204	203, 144	eqtr2d 2777	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅)))
205	5, 6, 7, 8, 27, 9, 53, 131, 14	israg 27639	. . . . 5 ⊢ (𝜑 → (⟨“𝑋𝑀𝑅”⟩ ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅))))
206	204, 205	mpbird 256	. . . 4 ⊢ (𝜑 → ⟨“𝑋𝑀𝑅”⟩ ∈ (∟G‘𝐺))
207	5, 6, 7, 8, 9, 13, 158, 160, 82, 161, 202, 157, 206	ragperp 27659	. . 3 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝑀))
208	5, 6, 7, 8, 9, 13, 158, 207	perpcom 27655	. 2 ⊢ (𝜑 → (𝑅𝐿𝑀)(⟂G‘𝐺)(𝐴𝐿𝐵))
209	2, 4, 51, 52, 153, 154, 208	reu2eqd 3694	1 ⊢ (𝜑 → 𝐵 = 𝑀)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∃!wreu 3351   class class class wbr 5105  ran crn 5634  ‘cfv 6496  (class class class)co 7357  ⟨“cs3 14731  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  Itvcitv 27375  LineGclng 27376  pInvGcmir 27594  ∟Gcrag 27635  ⟂Gcperpg 27637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-hash 14231  df-word 14403  df-concat 14459  df-s1 14484  df-s2 14737  df-s3 14738  df-trkgc 27390  df-trkgb 27391  df-trkgcb 27392  df-trkg 27395  df-cgrg 27453  df-leg 27525  df-mir 27595  df-rag 27636  df-perpg 27638

This theorem is referenced by:  opphllem  27677