oppperpex

Description: Restating colperpex using the "opposite side of a line" relation. (Contributed by Thierry Arnoux, 2-Aug-2020)

	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)$
	oppperpex.1	$⊢ φ \to A \in D$
	oppperpex.2	$⊢ φ \to C \in P$
	oppperpex.3	$⊢ φ \to \neg C \in D$
	oppperpex.4	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
Assertion	oppperpex	$⊢ φ \to \exists p \in P ((A L p) ⟂_{𝒢} (G) D \land C O p)$

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		oppperpex.1	$⊢ φ \to A \in D$
10		oppperpex.2	$⊢ φ \to C \in P$
11		oppperpex.3	$⊢ φ \to \neg C \in D$
12		oppperpex.4	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
13		simprrl	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to (A L p) ⟂_{𝒢} (G) (A L x)$
14	7	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to G \in 𝒢_{Tarski}$
15	6	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to D \in ran L$
16	9	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to A \in D$
17	1 5 3 14 15 16	tglnpt	$⊢ ((φ \land x \in D) \land A \neq x) \to A \in P$
18		simplr	$⊢ ((φ \land x \in D) \land A \neq x) \to x \in D$
19	1 5 3 14 15 18	tglnpt	$⊢ ((φ \land x \in D) \land A \neq x) \to x \in P$
20		simpr	$⊢ ((φ \land x \in D) \land A \neq x) \to A \neq x$
21	1 3 5 14 17 19 20 20 15 16 18	tglinethru	$⊢ ((φ \land x \in D) \land A \neq x) \to D = A L x$
22	21	adantr	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to D = A L x$
23	13 22	breqtrrd	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to (A L p) ⟂_{𝒢} (G) D$
24	11	ad3antrrr	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to \neg C \in D$
25	14	adantr	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to G \in 𝒢_{Tarski}$
26	15	adantr	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to D \in ran L$
27	16	adantr	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to A \in D$
28		simprl	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to p \in P$
29	1 2 3 5 25 26 27 28 23	footne	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to \neg p \in D$
30	20	ad3antrrr	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to A \neq x$
31	30	neneqd	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to \neg A = x$
32		simprrl	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to (t \in (A L x) \lor A = x)$
33	32	orcomd	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to (A = x \lor t \in (A L x))$
34	33	ord	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to (\neg A = x \to t \in (A L x))$
35	31 34	mpd	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to t \in (A L x)$
36	21	ad3antrrr	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to D = A L x$
37	35 36	eleqtrrd	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to t \in D$
38		simprrr	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to t \in (C I p)$
39	37 38	jca	$⊢ (((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \land (t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to (t \in D \land t \in (C I p))$
40	39	ex	$⊢ ((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \to ((t \in P \land ((t \in (A L x) \lor A = x) \land t \in (C I p))) \to (t \in D \land t \in (C I p)))$
41	40	reximdv2	$⊢ ((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \to (\exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p)) \to \exists t \in D t \in (C I p))$
42	41	impr	$⊢ ((((φ \land x \in D) \land A \neq x) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to \exists t \in D t \in (C I p)$
43	42	anasss	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to \exists t \in D t \in (C I p)$
44	24 29 43	jca31	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to ((\neg C \in D \land \neg p \in D) \land \exists t \in D t \in (C I p))$
45	10	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to C \in P$
46	45	ad2antrr	$⊢ ((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \to C \in P$
47		simplr	$⊢ ((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \to p \in P$
48	1 2 3 4 46 47	islnopp	$⊢ ((((φ \land x \in D) \land A \neq x) \land p \in P) \land (A L p) ⟂_{𝒢} (G) (A L x)) \to (C O p \leftrightarrow ((\neg C \in D \land \neg p \in D) \land \exists t \in D t \in (C I p)))$
49	48	adantrr	$⊢ ((((φ \land x \in D) \land A \neq x) \land p \in P) \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p)))) \to (C O p \leftrightarrow ((\neg C \in D \land \neg p \in D) \land \exists t \in D t \in (C I p)))$
50	49	anasss	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to (C O p \leftrightarrow ((\neg C \in D \land \neg p \in D) \land \exists t \in D t \in (C I p)))$
51	44 50	mpbird	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to C O p$
52	23 51	jca	$⊢ (((φ \land x \in D) \land A \neq x) \land (p \in P \land ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p))))) \to ((A L p) ⟂_{𝒢} (G) D \land C O p)$
53	12	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to G {Dim}_{𝒢} \geq 2$
54	1 2 3 5 14 17 19 45 20 53	colperpex	$⊢ ((φ \land x \in D) \land A \neq x) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L x) \land \exists t \in P ((t \in (A L x) \lor A = x) \land t \in (C I p)))$
55	52 54	reximddv	$⊢ ((φ \land x \in D) \land A \neq x) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) D \land C O p)$
56	1 3 5 7 6 9	tglnpt2	$⊢ φ \to \exists x \in D A \neq x$
57	55 56	r19.29a	$⊢ φ \to \exists p \in P ((A L p) ⟂_{𝒢} (G) D \land C O p)$

Metamath Proof Explorer

Theorem oppperpex

Proof