opphl

Description: If two points A and C lie on the opposite side of a line D then any point of the half line ( R A ) also lies opposite to C . Theorem 9.5 of Schwabhauser p. 69. (Contributed by Thierry Arnoux, 3-Mar-2019)

	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)$
	opphl.a	$⊢ φ \to A \in P$
	opphl.b	$⊢ φ \to B \in P$
	opphl.c	$⊢ φ \to C \in P$
	opphl.1	$⊢ φ \to A O C$
	opphl.2	$⊢ φ \to R \in D$
	opphl.3	$⊢ φ \to A K (R) B$
Assertion	opphl	$⊢ φ \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		opphl.k	$⊢ K = {hl}_{𝒢} (G)$
9		opphl.a	$⊢ φ \to A \in P$
10		opphl.b	$⊢ φ \to B \in P$
11		opphl.c	$⊢ φ \to C \in P$
12		opphl.1	$⊢ φ \to A O C$
13		opphl.2	$⊢ φ \to R \in D$
14		opphl.3	$⊢ φ \to A K (R) B$
15	6	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to D \in ran L$
16	7	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to G \in 𝒢_{Tarski}$
17		eqid	$⊢ {pInv}_{𝒢} (G) (m) = {pInv}_{𝒢} (G) (m)$
18	10	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to B \in P$
19		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
20		simp-4r	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to m \in P$
21	9	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A \in P$
22	1 2 3 5 19 16 20 17 21	mircl	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (m) (A) \in P$
23		simplr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to y \in D$
24		simp-6r	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to z \in D$
25	13	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to R \in D$
26	11	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to C \in P$
27		simp-8r	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to x \in D$
28	12	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A O C$
29		simp-7r	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to (A L x) ⟂_{𝒢} (G) D$
30	5 16 29	perpln1	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A L x \in ran L$
31	1 2 3 5 16 30 15 29	perpcom	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to D ⟂_{𝒢} (G) (A L x)$
32		simp-5r	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to (C L z) ⟂_{𝒢} (G) D$
33	5 16 32	perpln1	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to C L z \in ran L$
34	1 2 3 5 16 33 15 32	perpcom	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to D ⟂_{𝒢} (G) (C L z)$
35	1 5 3 16 15 27	tglnpt	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to x \in P$
36	1 3 5 16 21 35 30	tglnne	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A \neq x$
37	1 3 8 21 21 35 16 36	hlid	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A K (x) A$
38		simpllr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to z = {pInv}_{𝒢} (G) (m) (x)$
39	38	eqcomd	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (m) (x) = z$
40	1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 39	opphllem6	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to (A K (x) A \leftrightarrow {pInv}_{𝒢} (G) (m) (A) K (z) C)$
41	37 40	mpbid	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (m) (A) K (z) C$
42	1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 22 37 41	opphllem5	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A O {pInv}_{𝒢} (G) (m) (A)$
43	39 24	eqeltrd	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (m) (x) \in D$
44	1 2 3 5 19 16 17 15 20 27 43	mirln2	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to m \in D$
45	1 2 3 5 19 16 20 17 21	mirmir	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (m) ({pInv}_{𝒢} (G) (m) (A)) = A$
46	45	eqcomd	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A = {pInv}_{𝒢} (G) (m) ({pInv}_{𝒢} (G) (m) (A))$
47	1 5 3 7 6 13	tglnpt	$⊢ φ \to R \in P$
48	1 3 8 9 10 47 7 14	hlne1	$⊢ φ \to A \neq R$
49	48	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to A \neq R$
50	1 3 8 9 10 47 7 14	hlne2	$⊢ φ \to B \neq R$
51	50	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to B \neq R$
52	1 3 8 9 10 47 7	ishlg	$⊢ φ \to (A K (R) B \leftrightarrow (A \neq R \land B \neq R \land (A \in (R I B) \lor B \in (R I A))))$
53	14 52	mpbid	$⊢ φ \to (A \neq R \land B \neq R \land (A \in (R I B) \lor B \in (R I A)))$
54	53	simp3d	$⊢ φ \to (A \in (R I B) \lor B \in (R I A))$
55	54	ad8antr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to (A \in (R I B) \lor B \in (R I A))$
56	1 2 3 4 5 15 16 17 21 18 22 25 42 44 46 49 51 55	opphllem2	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to B O {pInv}_{𝒢} (G) (m) (A)$
57		simpr	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to (B L y) ⟂_{𝒢} (G) D$
58	5 16 57	perpln1	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to B L y \in ran L$
59	1 2 3 5 16 58 15 57	perpcom	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to D ⟂_{𝒢} (G) (B L y)$
60	1 5 3 16 15 24	tglnpt	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to z \in P$
61	1 3 8 22 26 60 16 41	hlne1	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (m) (A) \neq z$
62	1 3 8 22 26 60 16 5 41	hlln	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (m) (A) \in (C L z)$
63	1 3 5 16 26 60 33	tglnne	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to C \neq z$
64	1 3 5 16 26 60 63	tglinerflx2	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to z \in (C L z)$
65	1 3 5 16 22 60 61 61 33 62 64	tglinethru	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to C L z = {pInv}_{𝒢} (G) (m) (A) L z$
66	34 65	breqtrd	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to D ⟂_{𝒢} (G) ({pInv}_{𝒢} (G) (m) (A) L z)$
67	1 5 3 16 15 23	tglnpt	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to y \in P$
68	1 3 5 16 18 67 58	tglnne	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to B \neq y$
69	1 3 8 18 21 67 16 68	hlid	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to B K (y) B$
70	1 3 8 22 26 60 16 41	hlcomd	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to C K (z) {pInv}_{𝒢} (G) (m) (A)$
71	1 2 3 4 5 15 16 8 17 18 22 23 24 20 56 59 66 18 26 69 70	opphllem5	$⊢ ((((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \land y \in D) \land (B L y) ⟂_{𝒢} (G) D) \to B O C$
72	1 2 3 4 5 6 7 9 11 12	oppne1	$⊢ φ \to \neg A \in D$
73	1 3 8 9 10 47 7 5 14	hlln	$⊢ φ \to A \in (B L R)$
74	73	adantr	$⊢ (φ \land B \in D) \to A \in (B L R)$
75	7	adantr	$⊢ (φ \land B \in D) \to G \in 𝒢_{Tarski}$
76	10	adantr	$⊢ (φ \land B \in D) \to B \in P$
77	47	adantr	$⊢ (φ \land B \in D) \to R \in P$
78	50	adantr	$⊢ (φ \land B \in D) \to B \neq R$
79	6	adantr	$⊢ (φ \land B \in D) \to D \in ran L$
80		simpr	$⊢ (φ \land B \in D) \to B \in D$
81	13	adantr	$⊢ (φ \land B \in D) \to R \in D$
82	1 3 5 75 76 77 78 78 79 80 81	tglinethru	$⊢ (φ \land B \in D) \to D = B L R$
83	74 82	eleqtrrd	$⊢ (φ \land B \in D) \to A \in D$
84	72 83	mtand	$⊢ φ \to \neg B \in D$
85	1 2 3 5 7 6 10 84	footex	$⊢ φ \to \exists y \in D (B L y) ⟂_{𝒢} (G) D$
86	85	ad6antr	$⊢ ((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \to \exists y \in D (B L y) ⟂_{𝒢} (G) D$
87	71 86	r19.29a	$⊢ ((((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \land m \in P) \land z = {pInv}_{𝒢} (G) (m) (x)) \to B O C$
88	7	ad4antr	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to G \in 𝒢_{Tarski}$
89	6	ad4antr	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to D \in ran L$
90		simp-4r	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to x \in D$
91	1 5 3 88 89 90	tglnpt	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to x \in P$
92		simplr	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to z \in D$
93	1 5 3 88 89 92	tglnpt	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to z \in P$
94	1 2 3 4 5 6 7 9 11 12	opptgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
95	94	ad4antr	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to G {Dim}_{𝒢} \geq 2$
96	1 2 3 5 88 19 91 93 95	midex	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to \exists m \in P z = {pInv}_{𝒢} (G) (m) (x)$
97	87 96	r19.29a	$⊢ ((((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land z \in D) \land (C L z) ⟂_{𝒢} (G) D) \to B O C$
98	1 2 3 4 5 6 7 9 11 12	oppne2	$⊢ φ \to \neg C \in D$
99	1 2 3 5 7 6 11 98	footex	$⊢ φ \to \exists z \in D (C L z) ⟂_{𝒢} (G) D$
100	99	ad2antrr	$⊢ ((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to \exists z \in D (C L z) ⟂_{𝒢} (G) D$
101	97 100	r19.29a	$⊢ ((φ \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to B O C$
102	1 2 3 5 7 6 9 72	footex	$⊢ φ \to \exists x \in D (A L x) ⟂_{𝒢} (G) D$
103	101 102	r19.29a	$⊢ φ \to B O C$

Metamath Proof Explorer

Theorem opphl

Proof