oppcom

Description: Commutativity rule for "opposite" Theorem 9.2 of Schwabhauser p. 67. (Contributed by Thierry Arnoux, 19-Dec-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}$
	oppcom.a	$⊢ φ \to A \in P$
	oppcom.b	$⊢ φ \to B \in P$
	oppcom.o	$⊢ φ \to A O B$
Assertion	oppcom	$⊢ φ \to B O A$

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		oppcom.a	$⊢ φ \to A \in P$
9		oppcom.b	$⊢ φ \to B \in P$
10		oppcom.o	$⊢ φ \to A O B$
11	1 2 3 4 8 9	islnopp	$⊢ φ \to (A O B \leftrightarrow ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)))$
12	10 11	mpbid	$⊢ φ \to ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B))$
13	12	simpld	$⊢ φ \to (\neg A \in D \land \neg B \in D)$
14	13	simprd	$⊢ φ \to \neg B \in D$
15	13	simpld	$⊢ φ \to \neg A \in D$
16	12	simprd	$⊢ φ \to \exists t \in D t \in (A I B)$
17	7	ad2antrr	$⊢ ((φ \land t \in D) \land t \in (A I B)) \to G \in 𝒢_{Tarski}$
18	8	ad2antrr	$⊢ ((φ \land t \in D) \land t \in (A I B)) \to A \in P$
19	7	adantr	$⊢ (φ \land t \in D) \to G \in 𝒢_{Tarski}$
20	6	adantr	$⊢ (φ \land t \in D) \to D \in ran L$
21		simpr	$⊢ (φ \land t \in D) \to t \in D$
22	1 5 3 19 20 21	tglnpt	$⊢ (φ \land t \in D) \to t \in P$
23	22	adantr	$⊢ ((φ \land t \in D) \land t \in (A I B)) \to t \in P$
24	9	ad2antrr	$⊢ ((φ \land t \in D) \land t \in (A I B)) \to B \in P$
25		simpr	$⊢ ((φ \land t \in D) \land t \in (A I B)) \to t \in (A I B)$
26	1 2 3 17 18 23 24 25	tgbtwncom	$⊢ ((φ \land t \in D) \land t \in (A I B)) \to t \in (B I A)$
27	7	ad2antrr	$⊢ ((φ \land t \in D) \land t \in (B I A)) \to G \in 𝒢_{Tarski}$
28	9	ad2antrr	$⊢ ((φ \land t \in D) \land t \in (B I A)) \to B \in P$
29	22	adantr	$⊢ ((φ \land t \in D) \land t \in (B I A)) \to t \in P$
30	8	ad2antrr	$⊢ ((φ \land t \in D) \land t \in (B I A)) \to A \in P$
31		simpr	$⊢ ((φ \land t \in D) \land t \in (B I A)) \to t \in (B I A)$
32	1 2 3 27 28 29 30 31	tgbtwncom	$⊢ ((φ \land t \in D) \land t \in (B I A)) \to t \in (A I B)$
33	26 32	impbida	$⊢ (φ \land t \in D) \to (t \in (A I B) \leftrightarrow t \in (B I A))$
34	33	rexbidva	$⊢ φ \to (\exists t \in D t \in (A I B) \leftrightarrow \exists t \in D t \in (B I A))$
35	16 34	mpbid	$⊢ φ \to \exists t \in D t \in (B I A)$
36	14 15 35	jca31	$⊢ φ \to ((\neg B \in D \land \neg A \in D) \land \exists t \in D t \in (B I A))$
37	1 2 3 4 9 8	islnopp	$⊢ φ \to (B O A \leftrightarrow ((\neg B \in D \land \neg A \in D) \land \exists t \in D t \in (B I A)))$
38	36 37	mpbird	$⊢ φ \to B O A$

Metamath Proof Explorer

Theorem oppcom

Proof