mideulem2

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

	Ref	Expression
Hypotheses	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	mideulem2	⊢ ( 𝜑 → 𝐵 = 𝑀 )

Proof

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

Metamath Proof Explorer

Theorem mideulem2

Proof