hpgcom

Description: The half-plane relation commutes. Theorem 9.12 of Schwabhauser p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	hpgid.p	$⊢ P = {Base}_{G}$
	hpgid.i	$⊢ I = Itv (G)$
	hpgid.l	$⊢ L = {Line}_{𝒢} (G)$
	hpgid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	hpgid.d	$⊢ φ \to D \in ran L$
	hpgid.a	$⊢ φ \to A \in P$
	hpgid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	hpgcom.b	$⊢ φ \to B \in P$
	hpgcom.1	$⊢ φ \to A {hp}_{𝒢} (G) (D) B$
Assertion	hpgcom	$⊢ φ \to B {hp}_{𝒢} (G) (D) A$

Step	Hyp	Ref	Expression
1		hpgid.p	$⊢ P = {Base}_{G}$
2		hpgid.i	$⊢ I = Itv (G)$
3		hpgid.l	$⊢ L = {Line}_{𝒢} (G)$
4		hpgid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		hpgid.d	$⊢ φ \to D \in ran L$
6		hpgid.a	$⊢ φ \to A \in P$
7		hpgid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
8		hpgcom.b	$⊢ φ \to B \in P$
9		hpgcom.1	$⊢ φ \to A {hp}_{𝒢} (G) (D) B$
10		ancom	$⊢ (A O c \land B O c) \leftrightarrow (B O c \land A O c)$
11	10	a1i	$⊢ φ \to ((A O c \land B O c) \leftrightarrow (B O c \land A O c))$
12	11	rexbidv	$⊢ φ \to (\exists c \in P (A O c \land B O c) \leftrightarrow \exists c \in P (B O c \land A O c))$
13	1 2 3 7 4 5 6 8	hpgbr	$⊢ φ \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow \exists c \in P (A O c \land B O c))$
14	1 2 3 7 4 5 8 6	hpgbr	$⊢ φ \to (B {hp}_{𝒢} (G) (D) A \leftrightarrow \exists c \in P (B O c \land A O c))$
15	12 13 14	3bitr4d	$⊢ φ \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow B {hp}_{𝒢} (G) (D) A)$
16	9 15	mpbid	$⊢ φ \to B {hp}_{𝒢} (G) (D) A$

Metamath Proof Explorer