plngval

Description: The plane defined by a line A and a point R outside of A . This is defined as the union of 3 parts: the line itself, the open half-plane containing R , and the points opposite to R (see islnopp ). (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plngval.p	$⊢ P = {Base}_{G}$
	plngval.i	$⊢ I = Itv (G)$
	plngval.1	$⊢ L = {Line}_{𝒢} (G)$
	plngval.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	plngval.a	$⊢ φ \to A \in ran L$
	plngval.r	$⊢ φ \to R \in (P ∖ A)$
Assertion	plngval	$⊢ φ \to A E R = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\}$

Proof

Step	Hyp	Ref	Expression
1		plngval.p	$⊢ P = {Base}_{G}$
2		plngval.i	$⊢ I = Itv (G)$
3		plngval.1	$⊢ L = {Line}_{𝒢} (G)$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		plngval.a	$⊢ φ \to A \in ran L$
7		plngval.r	$⊢ φ \to R \in (P ∖ A)$
8		df-plng	Could not format PlnG = ( g e. _V \|-> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) \|-> { x e. ( Base ` g ) \| ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) ) : No typesetting found for \|- PlnG = ( g e. _V \|-> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) \|-> { x e. ( Base ` g ) \| ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) ) with typecode \|-
9		fveq2	$⊢ g = G \to {Line}_{𝒢} (g) = {Line}_{𝒢} (G)$
10	9 3	eqtr4di	$⊢ g = G \to {Line}_{𝒢} (g) = L$
11	10	rneqd	$⊢ g = G \to ran {Line}_{𝒢} (g) = ran L$
12		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
13	12 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
14	13	difeq1d	$⊢ g = G \to {Base}_{g} ∖ a = P ∖ a$
15		biidd	$⊢ g = G \to (x \in a \leftrightarrow x \in a)$
16		fveq2	$⊢ g = G \to {hp}_{𝒢} (g) = {hp}_{𝒢} (G)$
17	16	fveq1d	$⊢ g = G \to {hp}_{𝒢} (g) (a) = {hp}_{𝒢} (G) (a)$
18	17	breqd	$⊢ g = G \to (x {hp}_{𝒢} (g) (a) r \leftrightarrow x {hp}_{𝒢} (G) (a) r)$
19		fveq2	$⊢ g = G \to Itv (g) = Itv (G)$
20	19 2	eqtr4di	$⊢ g = G \to Itv (g) = I$
21	20	oveqd	$⊢ g = G \to x Itv (g) r = x I r$
22	21	eleq2d	$⊢ g = G \to (t \in (x Itv (g) r) \leftrightarrow t \in (x I r))$
23	22	rexbidv	$⊢ g = G \to (\exists t \in a t \in (x Itv (g) r) \leftrightarrow \exists t \in a t \in (x I r))$
24	15 18 23	3orbi123d	$⊢ g = G \to ((x \in a \lor x {hp}_{𝒢} (g) (a) r \lor \exists t \in a t \in (x Itv (g) r)) \leftrightarrow (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r)))$
25	13 24	rabeqbidv	$⊢ g = G \to \{x \in {Base}_{g} \| (x \in a \lor x {hp}_{𝒢} (g) (a) r \lor \exists t \in a t \in (x Itv (g) r))\} = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\}$
26	11 14 25	mpoeq123dv	$⊢ g = G \to (a \in ran {Line}_{𝒢} (g), r \in ({Base}_{g} ∖ a) ⟼ \{x \in {Base}_{g} \| (x \in a \lor x {hp}_{𝒢} (g) (a) r \lor \exists t \in a t \in (x Itv (g) r))\}) = (a \in ran L, r \in (P ∖ a) ⟼ \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\})$
27	5	elexd	$⊢ φ \to G \in V$
28	3	fvexi	$⊢ L \in V$
29	28	rnex	$⊢ ran L \in V$
30	29	a1i	$⊢ φ \to ran L \in V$
31	1	fvexi	$⊢ P \in V$
32	31	difexi	$⊢ P ∖ a \in V$
33	32	a1i	$⊢ (φ \land a \in ran L) \to P ∖ a \in V$
34	30 33	mpoexd	$⊢ φ \to (a \in ran L, r \in (P ∖ a) ⟼ \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\}) \in V$
35	8 26 27 34	fvmptd3	Could not format ( ph -> ( PlnG ` G ) = ( a e. ran L , r e. ( P \ a ) \|-> { x e. P \| ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) ) : No typesetting found for \|- ( ph -> ( PlnG ` G ) = ( a e. ran L , r e. ( P \ a ) \|-> { x e. P \| ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } ) ) with typecode \|-
36	4 35	eqtrid	$⊢ φ \to E = (a \in ran L, r \in (P ∖ a) ⟼ \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\})$
37	7	adantr	$⊢ (φ \land a = A) \to R \in (P ∖ A)$
38		difeq2	$⊢ a = A \to P ∖ a = P ∖ A$
39	38	adantl	$⊢ (φ \land a = A) \to P ∖ a = P ∖ A$
40	37 39	eleqtrrd	$⊢ (φ \land a = A) \to R \in (P ∖ a)$
41		eqid	$⊢ \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\} = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\}$
42	31	a1i	$⊢ (φ \land (a = A \land r = R)) \to P \in V$
43	41 42	rabexd	$⊢ (φ \land (a = A \land r = R)) \to \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\} \in V$
44		eleq2w2	$⊢ a = A \to (x \in a \leftrightarrow x \in A)$
45	44	ad2antrl	$⊢ (φ \land (a = A \land r = R)) \to (x \in a \leftrightarrow x \in A)$
46		eqidd	$⊢ (φ \land (a = A \land r = R)) \to x = x$
47		fveq2	$⊢ a = A \to {hp}_{𝒢} (G) (a) = {hp}_{𝒢} (G) (A)$
48	47	ad2antrl	$⊢ (φ \land (a = A \land r = R)) \to {hp}_{𝒢} (G) (a) = {hp}_{𝒢} (G) (A)$
49		simprr	$⊢ (φ \land (a = A \land r = R)) \to r = R$
50	46 48 49	breq123d	$⊢ (φ \land (a = A \land r = R)) \to (x {hp}_{𝒢} (G) (a) r \leftrightarrow x {hp}_{𝒢} (G) (A) R)$
51		simprl	$⊢ (φ \land (a = A \land r = R)) \to a = A$
52	49	oveq2d	$⊢ (φ \land (a = A \land r = R)) \to x I r = x I R$
53	52	eleq2d	$⊢ (φ \land (a = A \land r = R)) \to (t \in (x I r) \leftrightarrow t \in (x I R))$
54	51 53	rexeqbidv	$⊢ (φ \land (a = A \land r = R)) \to (\exists t \in a t \in (x I r) \leftrightarrow \exists t \in A t \in (x I R))$
55	45 50 54	3orbi123d	$⊢ (φ \land (a = A \land r = R)) \to ((x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r)) \leftrightarrow (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)))$
56	55	rabbidv	$⊢ (φ \land (a = A \land r = R)) \to \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\} = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\}$
57	6 40 43 56	ovmpodv2	$⊢ φ \to (E = (a \in ran L, r \in (P ∖ a) ⟼ \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\}) \to A E R = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\})$
58	36 57	mpd	$⊢ φ \to A E R = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\}$

Metamath Proof Explorer

Theorem plngval

Proof