opphllem4

	Ref	Expression
Hypotheses	hpg.p	$⊢ P = {Base}_{G}$
	hpg.d	$⊢ \underset{˙}{-} = dist (G)$
	hpg.i	$⊢ I = Itv (G)$
	hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	opphl.l	$⊢ L = {Line}_{𝒢} (G)$
	opphl.d	$⊢ φ \to D \in ran L$
	opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	opphl.k	$⊢ K = {hl}_{𝒢} (G)$
	opphllem5.n	$⊢ N = {pInv}_{𝒢} (G) (M)$
	opphllem5.a	$⊢ φ \to A \in P$
	opphllem5.c	$⊢ φ \to C \in P$
	opphllem5.r	$⊢ φ \to R \in D$
	opphllem5.s	$⊢ φ \to S \in D$
	opphllem5.m	$⊢ φ \to M \in P$
	opphllem5.o	$⊢ φ \to A O C$
	opphllem5.p	$⊢ φ \to D ⟂_{𝒢} (G) (A L R)$
	opphllem5.q	$⊢ φ \to D ⟂_{𝒢} (G) (C L S)$
	opphllem3.t	$⊢ φ \to R \neq S$
	opphllem3.l	$⊢ φ \to (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)$
	opphllem3.u	$⊢ φ \to U \in P$
	opphllem3.v	$⊢ φ \to N (R) = S$
	opphllem4.u	$⊢ φ \to V \in P$
	opphllem4.1	$⊢ φ \to U K (R) A$
	opphllem4.2	$⊢ φ \to V K (S) C$
Assertion	opphllem4	$⊢ φ \to U O V$

Proof

Step	Hyp	Ref	Expression
1		hpg.p	$⊢ P = {Base}_{G}$
2		hpg.d	$⊢ \underset{˙}{-} = dist (G)$
3		hpg.i	$⊢ I = Itv (G)$
4		hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		opphl.l	$⊢ L = {Line}_{𝒢} (G)$
6		opphl.d	$⊢ φ \to D \in ran L$
7		opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		opphl.k	$⊢ K = {hl}_{𝒢} (G)$
9		opphllem5.n	$⊢ N = {pInv}_{𝒢} (G) (M)$
10		opphllem5.a	$⊢ φ \to A \in P$
11		opphllem5.c	$⊢ φ \to C \in P$
12		opphllem5.r	$⊢ φ \to R \in D$
13		opphllem5.s	$⊢ φ \to S \in D$
14		opphllem5.m	$⊢ φ \to M \in P$
15		opphllem5.o	$⊢ φ \to A O C$
16		opphllem5.p	$⊢ φ \to D ⟂_{𝒢} (G) (A L R)$
17		opphllem5.q	$⊢ φ \to D ⟂_{𝒢} (G) (C L S)$
18		opphllem3.t	$⊢ φ \to R \neq S$
19		opphllem3.l	$⊢ φ \to (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)$
20		opphllem3.u	$⊢ φ \to U \in P$
21		opphllem3.v	$⊢ φ \to N (R) = S$
22		opphllem4.u	$⊢ φ \to V \in P$
23		opphllem4.1	$⊢ φ \to U K (R) A$
24		opphllem4.2	$⊢ φ \to V K (S) C$
25		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
26	1 2 3 5 25 7 14 9 20	mircl	$⊢ φ \to N (U) \in P$
27	1 5 3 7 6 13	tglnpt	$⊢ φ \to S \in P$
28	1 5 3 7 6 12	tglnpt	$⊢ φ \to R \in P$
29	18	necomd	$⊢ φ \to S \neq R$
30	1 2 3 5 25 7 14 9 28	mirbtwn	$⊢ φ \to M \in (N (R) I R)$
31	21	oveq1d	$⊢ φ \to N (R) I R = S I R$
32	30 31	eleqtrd	$⊢ φ \to M \in (S I R)$
33	1 3 5 7 27 28 14 29 32	btwnlng1	$⊢ φ \to M \in (S L R)$
34	1 3 5 7 27 28 29 29 6 13 12	tglinethru	$⊢ φ \to D = S L R$
35	33 34	eleqtrrd	$⊢ φ \to M \in D$
36	1 2 3 4 5 6 7 10 11 15	oppne1	$⊢ φ \to \neg A \in D$
37	1 3 8 20 10 28 7 23	hlne1	$⊢ φ \to U \neq R$
38	37	necomd	$⊢ φ \to R \neq U$
39	1 3 8 20 10 28 7 5 23	hlln	$⊢ φ \to U \in (A L R)$
40	1 3 8 20 10 28 7 23	hlne2	$⊢ φ \to A \neq R$
41	1 3 5 7 28 20 10 38 39 40	lnrot1	$⊢ φ \to A \in (R L U)$
42	41	adantr	$⊢ (φ \land U \in D) \to A \in (R L U)$
43	7	adantr	$⊢ (φ \land U \in D) \to G \in 𝒢_{Tarski}$
44	28	adantr	$⊢ (φ \land U \in D) \to R \in P$
45	20	adantr	$⊢ (φ \land U \in D) \to U \in P$
46	38	adantr	$⊢ (φ \land U \in D) \to R \neq U$
47	6	adantr	$⊢ (φ \land U \in D) \to D \in ran L$
48	12	adantr	$⊢ (φ \land U \in D) \to R \in D$
49		simpr	$⊢ (φ \land U \in D) \to U \in D$
50	1 3 5 43 44 45 46 46 47 48 49	tglinethru	$⊢ (φ \land U \in D) \to D = R L U$
51	42 50	eleqtrrd	$⊢ (φ \land U \in D) \to A \in D$
52	36 51	mtand	$⊢ φ \to \neg U \in D$
53	7	adantr	$⊢ (φ \land N (U) \in D) \to G \in 𝒢_{Tarski}$
54	14	adantr	$⊢ (φ \land N (U) \in D) \to M \in P$
55	20	adantr	$⊢ (φ \land N (U) \in D) \to U \in P$
56	1 2 3 5 25 53 54 9 55	mirmir	$⊢ (φ \land N (U) \in D) \to N (N (U)) = U$
57	6	adantr	$⊢ (φ \land N (U) \in D) \to D \in ran L$
58	35	adantr	$⊢ (φ \land N (U) \in D) \to M \in D$
59		simpr	$⊢ (φ \land N (U) \in D) \to N (U) \in D$
60	1 2 3 5 25 53 9 57 58 59	mirln	$⊢ (φ \land N (U) \in D) \to N (N (U)) \in D$
61	56 60	eqeltrrd	$⊢ (φ \land N (U) \in D) \to U \in D$
62	52 61	mtand	$⊢ φ \to \neg N (U) \in D$
63	1 2 3 5 25 7 14 9 20	mirbtwn	$⊢ φ \to M \in (N (U) I U)$
64	1 2 3 4 26 20 35 62 52 63	islnoppd	$⊢ φ \to N (U) O U$
65		eqidd	$⊢ φ \to N (U) = N (U)$
66	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	opphllem3	$⊢ φ \to (U K (R) A \leftrightarrow N (U) K (S) C)$
67	23 66	mpbid	$⊢ φ \to N (U) K (S) C$
68	1 3 8 22 11 27 7 24	hlcomd	$⊢ φ \to C K (S) V$
69	1 3 8 26 11 22 7 27 67 68	hltr	$⊢ φ \to N (U) K (S) V$
70	1 3 8 26 22 27 7	ishlg	$⊢ φ \to (N (U) K (S) V \leftrightarrow (N (U) \neq S \land V \neq S \land (N (U) \in (S I V) \lor V \in (S I N (U)))))$
71	69 70	mpbid	$⊢ φ \to (N (U) \neq S \land V \neq S \land (N (U) \in (S I V) \lor V \in (S I N (U))))$
72	71	simp1d	$⊢ φ \to N (U) \neq S$
73	1 3 8 11 22 27 7 68	hlne2	$⊢ φ \to V \neq S$
74	71	simp3d	$⊢ φ \to (N (U) \in (S I V) \lor V \in (S I N (U)))$
75	1 2 3 4 5 6 7 9 26 22 20 13 64 35 65 72 73 74	opphllem2	$⊢ φ \to V O U$
76	1 2 3 4 5 6 7 22 20 75	oppcom	$⊢ φ \to U O V$

Metamath Proof Explorer

Theorem opphllem4

Proof