opphllem2

	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}$
	opphllem1.s	$⊢ S = {pInv}_{𝒢} (G) (M)$
	opphllem1.a	$⊢ φ \to A \in P$
	opphllem1.b	$⊢ φ \to B \in P$
	opphllem1.c	$⊢ φ \to C \in P$
	opphllem1.r	$⊢ φ \to R \in D$
	opphllem1.o	$⊢ φ \to A O C$
	opphllem1.m	$⊢ φ \to M \in D$
	opphllem1.n	$⊢ φ \to A = S (C)$
	opphllem1.x	$⊢ φ \to A \neq R$
	opphllem1.y	$⊢ φ \to B \neq R$
	opphllem2.z	$⊢ φ \to (A \in (R I B) \lor B \in (R I A))$
Assertion	opphllem2	$⊢ φ \to B O C$

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		opphllem1.s	$⊢ S = {pInv}_{𝒢} (G) (M)$
9		opphllem1.a	$⊢ φ \to A \in P$
10		opphllem1.b	$⊢ φ \to B \in P$
11		opphllem1.c	$⊢ φ \to C \in P$
12		opphllem1.r	$⊢ φ \to R \in D$
13		opphllem1.o	$⊢ φ \to A O C$
14		opphllem1.m	$⊢ φ \to M \in D$
15		opphllem1.n	$⊢ φ \to A = S (C)$
16		opphllem1.x	$⊢ φ \to A \neq R$
17		opphllem1.y	$⊢ φ \to B \neq R$
18		opphllem2.z	$⊢ φ \to (A \in (R I B) \lor B \in (R I A))$
19	6	adantr	$⊢ (φ \land A \in (R I B)) \to D \in ran L$
20	7	adantr	$⊢ (φ \land A \in (R I B)) \to G \in 𝒢_{Tarski}$
21	11	adantr	$⊢ (φ \land A \in (R I B)) \to C \in P$
22	10	adantr	$⊢ (φ \land A \in (R I B)) \to B \in P$
23		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
24	1 5 3 7 6 14	tglnpt	$⊢ φ \to M \in P$
25	24	adantr	$⊢ (φ \land A \in (R I B)) \to M \in P$
26	1 2 3 5 23 20 25 8 22	mircl	$⊢ (φ \land A \in (R I B)) \to S (B) \in P$
27	14	adantr	$⊢ (φ \land A \in (R I B)) \to M \in D$
28	12	adantr	$⊢ (φ \land A \in (R I B)) \to R \in D$
29	1 2 3 5 23 20 8 19 27 28	mirln	$⊢ (φ \land A \in (R I B)) \to S (R) \in D$
30		simpr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A = B) \to A = B$
31		simplr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A = B) \to B \in D$
32	30 31	eqeltrd	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A = B) \to A \in D$
33	7	ad3antrrr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to G \in 𝒢_{Tarski}$
34	10	ad3antrrr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to B \in P$
35	1 5 3 7 6 12	tglnpt	$⊢ φ \to R \in P$
36	35	ad3antrrr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to R \in P$
37	9	ad3antrrr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to A \in P$
38	17	ad3antrrr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to B \neq R$
39	38	necomd	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to R \neq B$
40		simpllr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to A \in (R I B)$
41	1 3 5 33 36 34 37 39 40	btwnlng1	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to A \in (R L B)$
42	1 3 5 33 34 36 37 38 41	lncom	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to A \in (B L R)$
43	6	ad3antrrr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to D \in ran L$
44		simplr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to B \in D$
45	12	ad3antrrr	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to R \in D$
46	1 3 5 33 34 36 38 38 43 44 45	tglinethru	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to D = B L R$
47	42 46	eleqtrrd	$⊢ (((φ \land A \in (R I B)) \land B \in D) \land A \neq B) \to A \in D$
48	32 47	pm2.61dane	$⊢ ((φ \land A \in (R I B)) \land B \in D) \to A \in D$
49	1 2 3 4 5 6 7 9 11 13	oppne1	$⊢ φ \to \neg A \in D$
50	49	ad2antrr	$⊢ ((φ \land A \in (R I B)) \land B \in D) \to \neg A \in D$
51	48 50	pm2.65da	$⊢ (φ \land A \in (R I B)) \to \neg B \in D$
52	20	adantr	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to G \in 𝒢_{Tarski}$
53	25	adantr	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to M \in P$
54	22	adantr	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to B \in P$
55	1 2 3 5 23 52 53 8 54	mirmir	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to S (S (B)) = B$
56	19	adantr	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to D \in ran L$
57	27	adantr	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to M \in D$
58		simpr	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to S (B) \in D$
59	1 2 3 5 23 52 8 56 57 58	mirln	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to S (S (B)) \in D$
60	55 59	eqeltrrd	$⊢ ((φ \land A \in (R I B)) \land S (B) \in D) \to B \in D$
61	51 60	mtand	$⊢ (φ \land A \in (R I B)) \to \neg S (B) \in D$
62	1 2 3 5 23 20 25 8 22	mirbtwn	$⊢ (φ \land A \in (R I B)) \to M \in (S (B) I B)$
63	1 2 3 4 26 22 27 61 51 62	islnoppd	$⊢ (φ \land A \in (R I B)) \to S (B) O B$
64		eqidd	$⊢ (φ \land A \in (R I B)) \to S (B) = S (B)$
65		nelne2	$⊢ (S (R) \in D \land \neg S (B) \in D) \to S (R) \neq S (B)$
66	29 61 65	syl2anc	$⊢ (φ \land A \in (R I B)) \to S (R) \neq S (B)$
67	66	necomd	$⊢ (φ \land A \in (R I B)) \to S (B) \neq S (R)$
68	1 2 3 4 5 6 7 9 11 13	oppne2	$⊢ φ \to \neg C \in D$
69	68	adantr	$⊢ (φ \land A \in (R I B)) \to \neg C \in D$
70		nelne2	$⊢ (S (R) \in D \land \neg C \in D) \to S (R) \neq C$
71	29 69 70	syl2anc	$⊢ (φ \land A \in (R I B)) \to S (R) \neq C$
72	71	necomd	$⊢ (φ \land A \in (R I B)) \to C \neq S (R)$
73	15	eqcomd	$⊢ φ \to S (C) = A$
74	1 2 3 5 23 7 24 8 11 73	mircom	$⊢ φ \to S (A) = C$
75	74	adantr	$⊢ (φ \land A \in (R I B)) \to S (A) = C$
76	35	adantr	$⊢ (φ \land A \in (R I B)) \to R \in P$
77	9	adantr	$⊢ (φ \land A \in (R I B)) \to A \in P$
78		simpr	$⊢ (φ \land A \in (R I B)) \to A \in (R I B)$
79	1 2 3 5 23 20 25 8 76 77 22 78	mirbtwni	$⊢ (φ \land A \in (R I B)) \to S (A) \in (S (R) I S (B))$
80	75 79	eqeltrrd	$⊢ (φ \land A \in (R I B)) \to C \in (S (R) I S (B))$
81	1 2 3 4 5 19 20 8 26 21 22 29 63 27 64 67 72 80	opphllem1	$⊢ (φ \land A \in (R I B)) \to C O B$
82	1 2 3 4 5 19 20 21 22 81	oppcom	$⊢ (φ \land A \in (R I B)) \to B O C$
83	6	adantr	$⊢ (φ \land B \in (R I A)) \to D \in ran L$
84	7	adantr	$⊢ (φ \land B \in (R I A)) \to G \in 𝒢_{Tarski}$
85	9	adantr	$⊢ (φ \land B \in (R I A)) \to A \in P$
86	10	adantr	$⊢ (φ \land B \in (R I A)) \to B \in P$
87	11	adantr	$⊢ (φ \land B \in (R I A)) \to C \in P$
88	12	adantr	$⊢ (φ \land B \in (R I A)) \to R \in D$
89	13	adantr	$⊢ (φ \land B \in (R I A)) \to A O C$
90	14	adantr	$⊢ (φ \land B \in (R I A)) \to M \in D$
91	15	adantr	$⊢ (φ \land B \in (R I A)) \to A = S (C)$
92	16	adantr	$⊢ (φ \land B \in (R I A)) \to A \neq R$
93	17	adantr	$⊢ (φ \land B \in (R I A)) \to B \neq R$
94		simpr	$⊢ (φ \land B \in (R I A)) \to B \in (R I A)$
95	1 2 3 4 5 83 84 8 85 86 87 88 89 90 91 92 93 94	opphllem1	$⊢ (φ \land B \in (R I A)) \to B O C$
96	82 95 18	mpjaodan	$⊢ φ \to B O C$

Metamath Proof Explorer

Theorem opphllem2

Proof