Theorem opphllem4

Description: Lemma for opphl . (Contributed by Thierry Arnoux, 22-Feb-2020)

	Ref	Expression
Hypotheses	hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpg.d	⊢ − = ( dist ‘ 𝐺 )
	hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	opphl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	opphl.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	opphl.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	opphl.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	opphllem5.n	⊢ 𝑁 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
	opphllem5.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	opphllem5.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	opphllem5.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐷 )
	opphllem5.s	⊢ ( 𝜑 → 𝑆 ∈ 𝐷 )
	opphllem5.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
	opphllem5.o	⊢ ( 𝜑 → 𝐴 𝑂 𝐶 )
	opphllem5.p	⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
	opphllem5.q	⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
	opphllem3.t	⊢ ( 𝜑 → 𝑅 ≠ 𝑆 )
	opphllem3.l	⊢ ( 𝜑 → ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) )
	opphllem3.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
	opphllem3.v	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑅 ) = 𝑆 )
	opphllem4.u	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
	opphllem4.1	⊢ ( 𝜑 → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 )
	opphllem4.2	⊢ ( 𝜑 → 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 )
Assertion	opphllem4	⊢ ( 𝜑 → 𝑈 𝑂 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hpg.d	⊢ − = ( dist ‘ 𝐺 )
3		hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5		opphl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
6		opphl.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
7		opphl.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		opphl.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
9		opphllem5.n	⊢ 𝑁 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
10		opphllem5.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
11		opphllem5.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
12		opphllem5.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐷 )
13		opphllem5.s	⊢ ( 𝜑 → 𝑆 ∈ 𝐷 )
14		opphllem5.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
15		opphllem5.o	⊢ ( 𝜑 → 𝐴 𝑂 𝐶 )
16		opphllem5.p	⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) )
17		opphllem5.q	⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) )
18		opphllem3.t	⊢ ( 𝜑 → 𝑅 ≠ 𝑆 )
19		opphllem3.l	⊢ ( 𝜑 → ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) )
20		opphllem3.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
21		opphllem3.v	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑅 ) = 𝑆 )
22		opphllem4.u	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
23		opphllem4.1	⊢ ( 𝜑 → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 )
24		opphllem4.2	⊢ ( 𝜑 → 𝑉 ( 𝐾 ‘ 𝑆 ) 𝐶 )
25		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
26	1 2 3 5 25 7 14 9 20	mircl	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ∈ 𝑃 )
27	1 5 3 7 6 13	tglnpt	⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
28	1 5 3 7 6 12	tglnpt	⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
29	18	necomd	⊢ ( 𝜑 → 𝑆 ≠ 𝑅 )
30	1 2 3 5 25 7 14 9 28	mirbtwn	⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝑁 ‘ 𝑅 ) 𝐼 𝑅 ) )
31	21	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑅 ) 𝐼 𝑅 ) = ( 𝑆 𝐼 𝑅 ) )
32	30 31	eleqtrd	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑆 𝐼 𝑅 ) )
33	1 3 5 7 27 28 14 29 32	btwnlng1	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑆 𝐿 𝑅 ) )
34	1 3 5 7 27 28 29 29 6 13 12	tglinethru	⊢ ( 𝜑 → 𝐷 = ( 𝑆 𝐿 𝑅 ) )
35	33 34	eleqtrrd	⊢ ( 𝜑 → 𝑀 ∈ 𝐷 )
36	1 2 3 4 5 6 7 10 11 15	oppne1	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
37	1 3 8 20 10 28 7 23	hlne1	⊢ ( 𝜑 → 𝑈 ≠ 𝑅 )
38	37	necomd	⊢ ( 𝜑 → 𝑅 ≠ 𝑈 )
39	1 3 8 20 10 28 7 5 23	hlln	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 𝐿 𝑅 ) )
40	1 3 8 20 10 28 7 23	hlne2	⊢ ( 𝜑 → 𝐴 ≠ 𝑅 )
41	1 3 5 7 28 20 10 38 39 40	lnrot1	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 𝐿 𝑈 ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝐴 ∈ ( 𝑅 𝐿 𝑈 ) )
43	7	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
44	28	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝑅 ∈ 𝑃 )
45	20	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝑈 ∈ 𝑃 )
46	38	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝑅 ≠ 𝑈 )
47	6	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
48	12	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝑅 ∈ 𝐷 )
49		simpr	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝑈 ∈ 𝐷 )
50	1 3 5 43 44 45 46 46 47 48 49	tglinethru	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝐷 = ( 𝑅 𝐿 𝑈 ) )
51	42 50	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
52	36 51	mtand	⊢ ( 𝜑 → ¬ 𝑈 ∈ 𝐷 )
53	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
54	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → 𝑀 ∈ 𝑃 )
55	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → 𝑈 ∈ 𝑃 )
56	1 2 3 5 25 53 54 9 55	mirmir	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = 𝑈 )
57	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
58	35	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → 𝑀 ∈ 𝐷 )
59		simpr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 )
60	1 2 3 5 25 53 9 57 58 59	mirln	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) ∈ 𝐷 )
61	56 60	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 ) → 𝑈 ∈ 𝐷 )
62	52 61	mtand	⊢ ( 𝜑 → ¬ ( 𝑁 ‘ 𝑈 ) ∈ 𝐷 )
63	1 2 3 5 25 7 14 9 20	mirbtwn	⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝑁 ‘ 𝑈 ) 𝐼 𝑈 ) )
64	1 2 3 4 26 20 35 62 52 63	islnoppd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) 𝑂 𝑈 )
65		eqidd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) = ( 𝑁 ‘ 𝑈 ) )
66	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	opphllem3	⊢ ( 𝜑 → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) )
67	23 66	mpbid	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 )
68	1 3 8 22 11 27 7 24	hlcomd	⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝑆 ) 𝑉 )
69	1 3 8 26 11 22 7 27 67 68	hltr	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝑉 )
70	1 3 8 26 22 27 7	ishlg	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝑉 ↔ ( ( 𝑁 ‘ 𝑈 ) ≠ 𝑆 ∧ 𝑉 ≠ 𝑆 ∧ ( ( 𝑁 ‘ 𝑈 ) ∈ ( 𝑆 𝐼 𝑉 ) ∨ 𝑉 ∈ ( 𝑆 𝐼 ( 𝑁 ‘ 𝑈 ) ) ) ) ) )
71	69 70	mpbid	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ≠ 𝑆 ∧ 𝑉 ≠ 𝑆 ∧ ( ( 𝑁 ‘ 𝑈 ) ∈ ( 𝑆 𝐼 𝑉 ) ∨ 𝑉 ∈ ( 𝑆 𝐼 ( 𝑁 ‘ 𝑈 ) ) ) ) )
72	71	simp1d	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ≠ 𝑆 )
73	1 3 8 11 22 27 7 68	hlne2	⊢ ( 𝜑 → 𝑉 ≠ 𝑆 )
74	71	simp3d	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ∈ ( 𝑆 𝐼 𝑉 ) ∨ 𝑉 ∈ ( 𝑆 𝐼 ( 𝑁 ‘ 𝑈 ) ) ) )
75	1 2 3 4 5 6 7 9 26 22 20 13 64 35 65 72 73 74	opphllem2	⊢ ( 𝜑 → 𝑉 𝑂 𝑈 )
76	1 2 3 4 5 6 7 22 20 75	oppcom	⊢ ( 𝜑 → 𝑈 𝑂 𝑉 )