Theorem mideulem2 29267

Description: Lemma for opphllem 29268, which is itself used for mideu 29271. (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 7459	. . 3 ⊢ (𝑦 = 𝐵 → (𝑅𝐿𝑦) = (𝑅𝐿𝐵))
2	1	breq1d 5118	. 2 ⊢ (𝑦 = 𝐵 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵)))
3		oveq2 7459	. . 3 ⊢ (𝑦 = 𝑀 → (𝑅𝐿𝑦) = (𝑅𝐿𝑀))
4	3	breq1d 5118	. 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 29155	. . 3 ⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
14		opphllem.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
15	12	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ≠ 𝐵)
16	15	neneqd 2964	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝐴 = 𝐵)
17		mideulem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ 𝑃)
18		opphllem.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − 𝑂) = (𝐵 − 𝑅))
19		mideulem.6	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
20	8, 9, 19	perpln2 29243	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴𝐿𝑂) ∈ ran 𝐿)
21	5, 7, 8, 9, 10, 17, 20	tglnne 29153	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ 𝑂)
22	5, 6, 7, 9, 10, 17, 11, 14, 18, 21	tgcgrneq 29002	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ≠ 𝑅)
23	22	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ≠ 𝑅)
24	23	necomd 3014	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ≠ 𝐵)
25	24	neneqd 2964	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ 𝑅 = 𝐵)
26	16, 25	jca 521	. . . 4 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
27		mideu.s	. . . . . 6 ⊢ 𝑆 = (pInvG‘𝐺)
28	9	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
29	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃)
30	11	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃)
31	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑅 ∈ 𝑃)
32		mideulem.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
33		mideulem.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
34	8, 9, 33	perpln2 29243	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄𝐿𝐵) ∈ ran 𝐿)
35	5, 7, 8, 9, 32, 11, 34	tglnne 29153	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ≠ 𝐵)
36	5, 7, 8, 9, 32, 11, 35	tglinerflx2 29159	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (𝑄𝐿𝐵))
37	5, 6, 7, 8, 9, 13, 34, 33	perpcom 29245	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
38	5, 7, 8, 9, 10, 11, 12	tglinecom 29160	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
39	37, 38	breqtrd 5137	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄𝐿𝐵)(⟂G‘𝐺)(𝐵𝐿𝐴))
40	5, 6, 7, 8, 9, 32, 11, 36, 10, 39	perprag 29259	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑄𝐵𝐴”⟩ ∈ (∟G‘𝐺))
41		opphllem.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ (𝐵𝐼𝑄))
42	5, 8, 7, 9, 11, 14, 32, 41	btwncolg3 29077	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 ∈ (𝐵𝐿𝑅) ∨ 𝐵 = 𝑅))
43	5, 6, 7, 8, 27, 9, 32, 11, 10, 14, 40, 35, 42	ragcol 29231	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝑅𝐵𝐴”⟩ ∈ (∟G‘𝐺))
44	5, 6, 7, 8, 27, 9, 14, 11, 10, 43	ragcom 29230	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐴𝐵𝑅”⟩ ∈ (∟G‘𝐺))
45	44	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ⟨“𝐴𝐵𝑅”⟩ ∈ (∟G‘𝐺))
46		animorrl 996	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
47	5, 6, 7, 8, 27, 28, 29, 30, 31, 45, 46	ragflat3 29238	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → (𝐴 = 𝐵 ∨ 𝑅 = 𝐵))
48		oran 1005	. . . . 5 ⊢ ((𝐴 = 𝐵 ∨ 𝑅 = 𝐵) ↔ ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
49	47, 48	sylib 221	. . . 4 ⊢ ((𝜑 ∧ 𝑅 ∈ (𝐴𝐿𝐵)) → ¬ (¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵))
50	26, 49	pm2.65da 829	. . 3 ⊢ (𝜑 → ¬ 𝑅 ∈ (𝐴𝐿𝐵))
51	5, 6, 7, 8, 9, 13, 14, 50	foot 29254	. 2 ⊢ (𝜑 → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵))
52	5, 7, 8, 9, 10, 11, 12	tglinerflx2 29159	. 2 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐿𝐵))
53		mideulem2.1	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
54	12	neneqd 2964	. . . . 5 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
55		oveq2 7459	. . . . . . 7 ⊢ (𝑦 = 𝐴 → (𝑅𝐿𝑦) = (𝑅𝐿𝐴))
56	55	breq1d 5118	. . . . . 6 ⊢ (𝑦 = 𝐴 → ((𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵) ↔ (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵)))
57	51	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ∃!𝑦 ∈ (𝐴𝐿𝐵)(𝑅𝐿𝑦)(⟂G‘𝐺)(𝐴𝐿𝐵))
58	5, 7, 8, 9, 10, 11, 12	tglinerflx1 29158	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐿𝐵))
59	58	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐿𝐵))
60	52	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐵 ∈ (𝐴𝐿𝐵))
61	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
62	14	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ∈ 𝑃)
63	10	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃)
64	50, 54	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ 𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
65		pm4.56 1004	. . . . . . . . . . . 12 ⊢ ((¬ 𝑅 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵) ↔ ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
66	64, 65	sylib 221	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑅 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
67	5, 7, 8, 9, 14, 10, 11, 66	ncolne1 29150	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ≠ 𝐴)
68	67	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝐴)
69	5, 7, 8, 61, 62, 63, 68	tglinecom 29160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑅))
70	68	necomd 3014	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ≠ 𝑅)
71	17	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ 𝑃)
72	21	necomd 3014	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ≠ 𝐴)
73	72	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝐴)
74	53	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃)
75		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴)
76	75, 70	eqnetrd 3026	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ≠ 𝑅)
77		mideulem2.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (𝑅𝐼𝑂))
78	5, 6, 7, 9, 14, 53, 17, 77	tgbtwncom 29008	. . . . . . . . . . . . . . 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 29174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐿𝐵))
83	12	necomd 3014	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
84	83	neneqd 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 𝐵 = 𝐴)
85	84	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝐵 = 𝐴)
86	72	neneqd 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 𝑂 = 𝐴)
87	86	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝑂 = 𝐴)
88	85, 87	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
89	9	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐺 ∈ TarskiG)
90	11	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐵 ∈ 𝑃)
91	10	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝐴 ∈ 𝑃)
92	17	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂 ∈ 𝑃)
93	5, 7, 8, 9, 11, 10, 83	tglinerflx2 29159	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐴))
94	38, 19	eqbrtrrd 5135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝑂))
95	5, 6, 7, 8, 9, 11, 10, 93, 17, 94	perprag 29259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
96	95	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
97		animorrl 996	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝑂 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
98	5, 6, 7, 8, 27, 89, 90, 91, 92, 96, 97	ragflat3 29238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → (𝐵 = 𝐴 ∨ 𝑂 = 𝐴))
99		oran 1005	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = 𝐴 ∨ 𝑂 = 𝐴) ↔ ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
100	98, 99	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑂 ∈ (𝐵𝐿𝐴)) → ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
101	88, 100	pm2.65da 829	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
102	101, 38	neleqtrrd 2887	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
103		nelne2 3057	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑂 ∈ (𝐴𝐿𝐵)) → 𝑋 ≠ 𝑂)
104	82, 102, 103	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ≠ 𝑂)
105	5, 6, 7, 9, 17, 53, 14, 78, 104	tgbtwnne 29010	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑂 ≠ 𝑅)
106	105	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ≠ 𝑅)
107	106	necomd 3014	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑅 ≠ 𝑂)
108	77	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐼𝑂))
109	5, 7, 8, 61, 62, 71, 74, 107, 108	btwnlng1 29144	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ (𝑅𝐿𝑂))
110	5, 7, 8, 61, 74, 62, 71, 76, 109, 107	lnrot2 29149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝑋𝐿𝑅))
111	75	oveq1d 7466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑋𝐿𝑅) = (𝐴𝐿𝑅))
112	110, 111	eleqtrd 2866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑂 ∈ (𝐴𝐿𝑅))
113	5, 7, 8, 61, 63, 62, 70, 71, 73, 112	tglineelsb2 29157	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑅) = (𝐴𝐿𝑂))
114	69, 113	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴) = (𝐴𝐿𝑂))
115	5, 6, 7, 8, 9, 13, 20, 19	perpcom 29245	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵))
116	115	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝑂)(⟂G‘𝐺)(𝐴𝐿𝐵))
117	114, 116	eqbrtrd 5133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝐵))
118	13	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵) ∈ ran 𝐿)
119	22	necomd 3014	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ 𝐵)
120	5, 7, 8, 9, 14, 11, 119	tgelrnln 29155	. . . . . . . 8 ⊢ (𝜑 → (𝑅𝐿𝐵) ∈ ran 𝐿)
121	120	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵) ∈ ran 𝐿)
122	5, 7, 8, 9, 14, 11, 119	tglinerflx2 29159	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐿𝐵))
123	52, 122	elind 4100	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝐵)))
124	5, 7, 8, 9, 14, 11, 119	tglinerflx1 29158	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝐵))
125	5, 6, 7, 8, 9, 13, 120, 123, 58, 124, 12, 119, 44	ragperp 29249	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵))
126	125	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝐵))
127	5, 6, 7, 8, 61, 118, 121, 126	perpcom 29245	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
128	56, 2, 57, 59, 60, 117, 127	reu2eqd 3697	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝐵)
129	54, 128	mtand 828	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐴)
130	129	neqned 2966	. . 3 ⊢ (𝜑 → 𝑋 ≠ 𝐴)
131		mideulem2.7	. . 3 ⊢ (𝜑 → 𝑀 ∈ 𝑃)
132	130	necomd 3014	. . . 4 ⊢ (𝜑 → 𝐴 ≠ 𝑋)
133		eqid 2763	. . . . 5 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
134		eqid 2763	. . . . 5 ⊢ (𝑆‘𝑀) = (𝑆‘𝑀)
135	5, 6, 7, 8, 27, 9, 10, 133, 17	mircl 29190	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃)
136		mideulem2.4	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
137		mideulem2.5	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
138	82	orcd 887	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
139	5, 8, 7, 9, 10, 11, 53, 138	colcom 29078	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
140	5, 8, 7, 9, 11, 10, 53, 139	colrot1 29079	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
141	5, 6, 7, 8, 27, 9, 11, 10, 17, 53, 95, 83, 140	ragcol 29231	. . . . . 6 ⊢ (𝜑 → ⟨“𝑋𝐴𝑂”⟩ ∈ (∟G‘𝐺))
142	5, 6, 7, 8, 27, 9, 53, 10, 17	israg 29229	. . . . . 6 ⊢ (𝜑 → (⟨“𝑋𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂))))
143	141, 142	mpbid 235	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
144		mideulem2.6	. . . . . 6 ⊢ (𝜑 → (𝑋 − 𝑍) = (𝑋 − 𝑅))
145	144	eqcomd 2769	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑅) = (𝑋 − 𝑍))
146		eqidd 2764	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝑂) = ((𝑆‘𝐴)‘𝑂))
147		mideulem2.8	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = ((𝑆‘𝑀)‘𝑍))
148	147	eqcomd 2769	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝑀)‘𝑍) = 𝑅)
149	5, 6, 7, 8, 27, 9, 131, 134, 136, 148	mircom 29192	. . . . . 6 ⊢ (𝜑 → ((𝑆‘𝑀)‘𝑅) = 𝑍)
150	149	eqcomd 2769	. . . . 5 ⊢ (𝜑 → 𝑍 = ((𝑆‘𝑀)‘𝑅))
151	5, 6, 7, 8, 27, 9, 133, 134, 17, 135, 53, 14, 136, 10, 131, 78, 137, 143, 145, 146, 150	krippen 29220	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐼𝑀))
152	5, 7, 8, 9, 10, 53, 131, 132, 151	btwnlng3 29146	. . 3 ⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝑋))
153	5, 7, 8, 9, 10, 11, 12, 53, 130, 82, 131, 152	tglineeltr 29156	. 2 ⊢ (𝜑 → 𝑀 ∈ (𝐴𝐿𝐵))
154	5, 6, 7, 8, 9, 13, 120, 125	perpcom 29245	. 2 ⊢ (𝜑 → (𝑅𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝐵))
155		nelne2 3057	. . . . . 6 ⊢ ((𝑀 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑅 ∈ (𝐴𝐿𝐵)) → 𝑀 ≠ 𝑅)
156	153, 50, 155	syl2anc 596	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝑅)
157	156	necomd 3014	. . . 4 ⊢ (𝜑 → 𝑅 ≠ 𝑀)
158	5, 7, 8, 9, 14, 131, 157	tgelrnln 29155	. . 3 ⊢ (𝜑 → (𝑅𝐿𝑀) ∈ ran 𝐿)
159	5, 7, 8, 9, 14, 131, 157	tglinerflx2 29159	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (𝑅𝐿𝑀))
160	153, 159	elind 4100	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ((𝐴𝐿𝐵) ∩ (𝑅𝐿𝑀)))
161	5, 7, 8, 9, 14, 131, 157	tglinerflx1 29158	. . . 4 ⊢ (𝜑 → 𝑅 ∈ (𝑅𝐿𝑀))
162		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝑋)
163	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐺 ∈ TarskiG)
164	131	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ 𝑃)
165	10	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝐴 ∈ 𝑃)
166	17	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑂 ∈ 𝑃)
167	135	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) ∈ 𝑃)
168	143	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑋 − 𝑂) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
169	162	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑂) = (𝑋 − 𝑂))
170	162	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑋 − ((𝑆‘𝐴)‘𝑂)))
171	168, 169, 170	3eqtr4rd 2809	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝐴)‘𝑂)) = (𝑀 − 𝑂))
172	136	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ∈ 𝑃)
173	14	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ∈ 𝑃)
174	147	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 = ((𝑆‘𝑀)‘𝑍))
175	174	oveq2d 7467	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − ((𝑆‘𝑀)‘𝑍)))
176	5, 6, 7, 8, 27, 163, 164, 134, 172	mircgr 29186	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − ((𝑆‘𝑀)‘𝑍)) = (𝑀 − 𝑍))
177	175, 176	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑀 − 𝑅) = (𝑀 − 𝑍))
178	5, 6, 7, 163, 164, 173, 164, 172, 177	tgcgrcomlr 28999	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → (𝑅 − 𝑀) = (𝑍 − 𝑀))
179	82	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝐴𝐿𝐵))
180	162, 179	eqeltrd 2864	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝐴𝐿𝐵))
181	50	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ¬ 𝑅 ∈ (𝐴𝐿𝐵))
182	180, 181, 155	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ≠ 𝑅)
183	182	necomd 3014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑅 ≠ 𝑀)
184	5, 6, 7, 163, 173, 164, 172, 164, 178, 183	tgcgrneq 29002	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑍 ≠ 𝑀)
185	5, 6, 7, 8, 27, 9, 131, 134, 136	mirbtwn 29187	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (((𝑆‘𝑀)‘𝑍)𝐼𝑍))
186	147	oveq1d 7466	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅𝐼𝑍) = (((𝑆‘𝑀)‘𝑍)𝐼𝑍))
187	185, 186	eleqtrrd 2867	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝑅𝐼𝑍))
188	187	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑍))
189	5, 6, 7, 163, 173, 164, 172, 188	tgbtwncom 29008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼𝑅))
190	137	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
191	162, 190	eqeltrd 2864	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑍))
192	5, 6, 7, 163, 167, 164, 172, 191	tgbtwncom 29008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑍𝐼((𝑆‘𝐴)‘𝑂)))
193	77	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 ∈ (𝑅𝐼𝑂))
194	162, 193	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (𝑅𝐼𝑂))
195	5, 7, 163, 172, 164, 173, 167, 166, 184, 183, 189, 192, 194	tgbtwnconn22 29099	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 ∈ (((𝑆‘𝐴)‘𝑂)𝐼𝑂))
196	5, 6, 7, 8, 27, 163, 164, 134, 166, 167, 171, 195	ismir 29188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝐴)‘𝑂) = ((𝑆‘𝑀)‘𝑂))
197	196	eqcomd 2769	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → ((𝑆‘𝑀)‘𝑂) = ((𝑆‘𝐴)‘𝑂))
198	5, 6, 7, 8, 27, 163, 164, 165, 166, 197	miduniq1 29215	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑀 = 𝐴)
199	162, 198	eqtr3d 2800	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑀 = 𝑋) → 𝑋 = 𝐴)
200	129, 199	mtand 828	. . . . . 6 ⊢ (𝜑 → ¬ 𝑀 = 𝑋)
201	200	neqned 2966	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝑋)
202	201	necomd 3014	. . . 4 ⊢ (𝜑 → 𝑋 ≠ 𝑀)
203	149	oveq2d 7467	. . . . . 6 ⊢ (𝜑 → (𝑋 − ((𝑆‘𝑀)‘𝑅)) = (𝑋 − 𝑍))
204	203, 144	eqtr2d 2799	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅)))
205	5, 6, 7, 8, 27, 9, 53, 131, 14	israg 29229	. . . . 5 ⊢ (𝜑 → (⟨“𝑋𝑀𝑅”⟩ ∈ (∟G‘𝐺) ↔ (𝑋 − 𝑅) = (𝑋 − ((𝑆‘𝑀)‘𝑅))))
206	204, 205	mpbird 260	. . . 4 ⊢ (𝜑 → ⟨“𝑋𝑀𝑅”⟩ ∈ (∟G‘𝐺))
207	5, 6, 7, 8, 9, 13, 158, 160, 82, 161, 202, 157, 206	ragperp 29249	. . 3 ⊢ (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑅𝐿𝑀))
208	5, 6, 7, 8, 9, 13, 158, 207	perpcom 29245	. 2 ⊢ (𝜑 → (𝑅𝐿𝑀)(⟂G‘𝐺)(𝐴𝐿𝐵))
209	2, 4, 51, 52, 153, 154, 208	reu2eqd 3697	1 ⊢ (𝜑 → 𝐵 = 𝑀)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∃!wreu 3367   class class class wbr 5108  ran crn 5659  ‘cfv 6566  (class class class)co 7451  ⟨“cs3 15035  Basecbs 17431  distcds 17481  TarskiGcstrkg 28946  Itvcitv 28952  LineGclng 28953  pInvGcmir 29181  ∟Gcrag 29225  ⟂Gcperpg 29227

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-1st 8035  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-oadd 8518  df-er 8755  df-map 8887  df-pm 8888  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-dju 10019  df-card 10057  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-nn 12376  df-2 12445  df-3 12446  df-n0 12647  df-xnn0 12720  df-z 12734  df-uz 13006  df-fz 13680  df-fzo 13829  df-hash 14516  df-word 14700  df-concat 14757  df-s1 14784  df-s2 15041  df-s3 15042  df-trkgc 28967  df-trkgb 28968  df-trkgcb 28969  df-trkg 28972  df-cgrg 29031  df-leg 29103  df-mir 29182  df-rag 29226  df-perpg 29228

This theorem is used by:  opphllem  29268