Theorem hpgbr

Description: Half-planes : property for points A and B to belong to the same open half plane delimited by line D . Definition 9.7 of Schwabhauser p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	ishpg.p	$$⊢P={\mathrm{Base}}_G$$
	ishpg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	ishpg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	ishpg.o	$$⊢O=\left\{⟨a,b⟩|\left(\left(a\in \left(P\setminus D\right)\wedge b\in \left(P\setminus D\right)\right)\wedge \exists t\in Dt\in \left(aIb\right)\right)\right\}$$
	ishpg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	ishpg.d	$$⊢\phi \to D\in \mathrm{ran}L$$
	hpgbr.a	$$⊢\phi \to A\in P$$
	hpgbr.b	$$⊢\phi \to B\in P$$
Assertion	hpgbr	$$⊢\phi \to \left(A{hp}_{𝒢}\left(G\right)\left(D\right)B\leftrightarrow \exists c\in P\left(AOc\wedge BOc\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ishpg.p	$$⊢P={\mathrm{Base}}_G$$
2		ishpg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		ishpg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
4		ishpg.o	$$⊢O=\left\{⟨a,b⟩|\left(\left(a\in \left(P\setminus D\right)\wedge b\in \left(P\setminus D\right)\right)\wedge \exists t\in Dt\in \left(aIb\right)\right)\right\}$$
5		ishpg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		ishpg.d	$$⊢\phi \to D\in \mathrm{ran}L$$
7		hpgbr.a	$$⊢\phi \to A\in P$$
8		hpgbr.b	$$⊢\phi \to B\in P$$
9	1 2 3 4 5 6	ishpg	$$⊢\phi \to {hp}_{𝒢}\left(G\right)\left(D\right)=\left\{⟨a,b⟩|\exists c\in P\left(aOc\wedge bOc\right)\right\}$$
10		simpl	$$⊢\left(a=u\wedge b=v\right)\to a=u$$
11	10	breq1d	$$⊢\left(a=u\wedge b=v\right)\to \left(aOc\leftrightarrow uOc\right)$$
12		simpr	$$⊢\left(a=u\wedge b=v\right)\to b=v$$
13	12	breq1d	$$⊢\left(a=u\wedge b=v\right)\to \left(bOc\leftrightarrow vOc\right)$$
14	11 13	anbi12d	$$⊢\left(a=u\wedge b=v\right)\to \left(\left(aOc\wedge bOc\right)\leftrightarrow \left(uOc\wedge vOc\right)\right)$$
15	14	rexbidv	$$⊢\left(a=u\wedge b=v\right)\to \left(\exists c\in P\left(aOc\wedge bOc\right)\leftrightarrow \exists c\in P\left(uOc\wedge vOc\right)\right)$$
16	15	cbvopabv	$$⊢\left\{⟨a,b⟩|\exists c\in P\left(aOc\wedge bOc\right)\right\}=\left\{⟨u,v⟩|\exists c\in P\left(uOc\wedge vOc\right)\right\}$$
17	9 16	eqtrdi	$$⊢\phi \to {hp}_{𝒢}\left(G\right)\left(D\right)=\left\{⟨u,v⟩|\exists c\in P\left(uOc\wedge vOc\right)\right\}$$
18	17	breqd	$$⊢\phi \to \left(A{hp}_{𝒢}\left(G\right)\left(D\right)B\leftrightarrow A\left\{⟨u,v⟩|\exists c\in P\left(uOc\wedge vOc\right)\right\}B\right)$$
19		simpl	$$⊢\left(u=A\wedge v=B\right)\to u=A$$
20	19	breq1d	$$⊢\left(u=A\wedge v=B\right)\to \left(uOc\leftrightarrow AOc\right)$$
21		simpr	$$⊢\left(u=A\wedge v=B\right)\to v=B$$
22	21	breq1d	$$⊢\left(u=A\wedge v=B\right)\to \left(vOc\leftrightarrow BOc\right)$$
23	20 22	anbi12d	$$⊢\left(u=A\wedge v=B\right)\to \left(\left(uOc\wedge vOc\right)\leftrightarrow \left(AOc\wedge BOc\right)\right)$$
24	23	rexbidv	$$⊢\left(u=A\wedge v=B\right)\to \left(\exists c\in P\left(uOc\wedge vOc\right)\leftrightarrow \exists c\in P\left(AOc\wedge BOc\right)\right)$$
25		eqid	$$⊢\left\{⟨u,v⟩|\exists c\in P\left(uOc\wedge vOc\right)\right\}=\left\{⟨u,v⟩|\exists c\in P\left(uOc\wedge vOc\right)\right\}$$
26	24 25	brabga	$$⊢\left(A\in P\wedge B\in P\right)\to \left(A\left\{⟨u,v⟩|\exists c\in P\left(uOc\wedge vOc\right)\right\}B\leftrightarrow \exists c\in P\left(AOc\wedge BOc\right)\right)$$
27	7 8 26	syl2anc	$$⊢\phi \to \left(A\left\{⟨u,v⟩|\exists c\in P\left(uOc\wedge vOc\right)\right\}B\leftrightarrow \exists c\in P\left(AOc\wedge BOc\right)\right)$$
28	18 27	bitrd	$$⊢\phi \to \left(A{hp}_{𝒢}\left(G\right)\left(D\right)B\leftrightarrow \exists c\in P\left(AOc\wedge BOc\right)\right)$$