opphllem1

	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$
	opphllem1.z	$⊢ φ \to B \in (R I A)$
Assertion	opphllem1	$⊢ φ \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		opphllem1.z	$⊢ φ \to B \in (R I A)$
19	1 2 3 4 5 6 7 9 11 13	oppne1	$⊢ φ \to \neg A \in D$
20		simpr	$⊢ ((φ \land B \in D) \land A = B) \to A = B$
21		simplr	$⊢ ((φ \land B \in D) \land A = B) \to B \in D$
22	20 21	eqeltrd	$⊢ ((φ \land B \in D) \land A = B) \to A \in D$
23	7	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to G \in 𝒢_{Tarski}$
24	10	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to B \in P$
25	1 5 3 7 6 12	tglnpt	$⊢ φ \to R \in P$
26	25	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to R \in P$
27	9	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to A \in P$
28	17	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to B \neq R$
29	28	necomd	$⊢ ((φ \land B \in D) \land A \neq B) \to R \neq B$
30	18	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to B \in (R I A)$
31	1 3 5 23 26 24 27 29 30	btwnlng3	$⊢ ((φ \land B \in D) \land A \neq B) \to A \in (R L B)$
32	1 3 5 23 24 26 27 28 31	lncom	$⊢ ((φ \land B \in D) \land A \neq B) \to A \in (B L R)$
33	6	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to D \in ran L$
34		simplr	$⊢ ((φ \land B \in D) \land A \neq B) \to B \in D$
35	12	ad2antrr	$⊢ ((φ \land B \in D) \land A \neq B) \to R \in D$
36	1 3 5 23 24 26 28 28 33 34 35	tglinethru	$⊢ ((φ \land B \in D) \land A \neq B) \to D = B L R$
37	32 36	eleqtrrd	$⊢ ((φ \land B \in D) \land A \neq B) \to A \in D$
38	22 37	pm2.61dane	$⊢ (φ \land B \in D) \to A \in D$
39	19 38	mtand	$⊢ φ \to \neg B \in D$
40	1 2 3 4 5 6 7 9 11 13	oppne2	$⊢ φ \to \neg C \in D$
41	1 5 3 7 6 14	tglnpt	$⊢ φ \to M \in P$
42		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
43	1 2 3 5 42 7 41 8 9	mirbtwn	$⊢ φ \to M \in (S (A) I A)$
44	15	eqcomd	$⊢ φ \to S (C) = A$
45	1 2 3 5 42 7 41 8 11 44	mircom	$⊢ φ \to S (A) = C$
46	45	oveq1d	$⊢ φ \to S (A) I A = C I A$
47	43 46	eleqtrd	$⊢ φ \to M \in (C I A)$
48	1 2 3 7 25 11 9 10 41 18 47	axtgpasch	$⊢ φ \to \exists t \in P (t \in (B I C) \land t \in (M I R))$
49	7	ad2antrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to G \in 𝒢_{Tarski}$
50	25	ad2antrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to R \in P$
51		simplrl	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to t \in P$
52		simplrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to (t \in (B I C) \land t \in (M I R))$
53	52	simprd	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to t \in (M I R)$
54		simpr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to M = R$
55	54	oveq1d	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to M I R = R I R$
56	53 55	eleqtrd	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to t \in (R I R)$
57	1 2 3 49 50 51 56	axtgbtwnid	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to R = t$
58	12	ad2antrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to R \in D$
59	57 58	eqeltrrd	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M = R) \to t \in D$
60	7	ad2antrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to G \in 𝒢_{Tarski}$
61	41	ad2antrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to M \in P$
62	25	ad2antrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to R \in P$
63		simplrl	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to t \in P$
64		simpr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to M \neq R$
65		simplrr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to (t \in (B I C) \land t \in (M I R))$
66	65	simprd	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to t \in (M I R)$
67	1 3 5 60 61 62 63 64 66	btwnlng1	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to t \in (M L R)$
68	7	adantr	$⊢ (φ \land M \neq R) \to G \in 𝒢_{Tarski}$
69	41	adantr	$⊢ (φ \land M \neq R) \to M \in P$
70	25	adantr	$⊢ (φ \land M \neq R) \to R \in P$
71		simpr	$⊢ (φ \land M \neq R) \to M \neq R$
72	6	adantr	$⊢ (φ \land M \neq R) \to D \in ran L$
73	14	adantr	$⊢ (φ \land M \neq R) \to M \in D$
74	12	adantr	$⊢ (φ \land M \neq R) \to R \in D$
75	1 3 5 68 69 70 71 71 72 73 74	tglinethru	$⊢ (φ \land M \neq R) \to D = M L R$
76	75	adantlr	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to D = M L R$
77	67 76	eleqtrrd	$⊢ ((φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \land M \neq R) \to t \in D$
78	59 77	pm2.61dane	$⊢ (φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \to t \in D$
79		simprrl	$⊢ (φ \land (t \in P \land (t \in (B I C) \land t \in (M I R)))) \to t \in (B I C)$
80	48 78 79	reximssdv	$⊢ φ \to \exists t \in D t \in (B I C)$
81	39 40 80	jca31	$⊢ φ \to ((\neg B \in D \land \neg C \in D) \land \exists t \in D t \in (B I C))$
82	1 2 3 4 10 11	islnopp	$⊢ φ \to (B O C \leftrightarrow ((\neg B \in D \land \neg C \in D) \land \exists t \in D t \in (B I C)))$
83	81 82	mpbird	$⊢ φ \to B O C$

Metamath Proof Explorer

Theorem opphllem1

Proof