isplng

Description: The property of being a plane. (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}$
	isplng.h	$⊢ φ \to H \in ran E$
Assertion	isplng	$⊢ φ \to \exists a \in ran L \exists r \in (P ∖ a) H = a E 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		isplng.h	$⊢ φ \to H \in ran E$
7		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 \|-
8		fveq2	$⊢ g = G \to {Line}_{𝒢} (g) = {Line}_{𝒢} (G)$
9	8 3	eqtr4di	$⊢ g = G \to {Line}_{𝒢} (g) = L$
10	9	rneqd	$⊢ g = G \to ran {Line}_{𝒢} (g) = ran L$
11		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
12	11 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
13	12	difeq1d	$⊢ g = G \to {Base}_{g} ∖ a = P ∖ a$
14		biidd	$⊢ g = G \to (x \in a \leftrightarrow x \in a)$
15		fveq2	$⊢ g = G \to {hp}_{𝒢} (g) = {hp}_{𝒢} (G)$
16	15	fveq1d	$⊢ g = G \to {hp}_{𝒢} (g) (a) = {hp}_{𝒢} (G) (a)$
17	16	breqd	$⊢ g = G \to (x {hp}_{𝒢} (g) (a) r \leftrightarrow x {hp}_{𝒢} (G) (a) r)$
18		fveq2	$⊢ g = G \to Itv (g) = Itv (G)$
19	18 2	eqtr4di	$⊢ g = G \to Itv (g) = I$
20	19	oveqd	$⊢ g = G \to x Itv (g) r = x I r$
21	20	eleq2d	$⊢ g = G \to (t \in (x Itv (g) r) \leftrightarrow t \in (x I r))$
22	21	rexbidv	$⊢ g = G \to (\exists t \in a t \in (x Itv (g) r) \leftrightarrow \exists t \in a t \in (x I r))$
23	14 17 22	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)))$
24	12 23	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))\}$
25	10 13 24	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))\})$
26	5	elexd	$⊢ φ \to G \in V$
27	3	fvexi	$⊢ L \in V$
28	27	rnex	$⊢ ran L \in V$
29	28	a1i	$⊢ φ \to ran L \in V$
30	1	fvexi	$⊢ P \in V$
31	30	difexi	$⊢ P ∖ a \in V$
32	31	a1i	$⊢ (φ \land a \in ran L) \to P ∖ a \in V$
33	29 32	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$
34	7 25 26 33	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 \|-
35	4 34	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))\})$
36	35	rneqd	$⊢ φ \to ran E = ran (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	6 36	eleqtrd	$⊢ φ \to H \in ran (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))\})$
38		eqid	$⊢ (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))\}) = (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))\})$
39	30	rabex	$⊢ \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\} \in V$
40	38 39	elrnmpo	$⊢ H \in ran (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))\}) \leftrightarrow \exists a \in ran L \exists r \in (P ∖ a) H = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\}$
41	37 40	sylib	$⊢ φ \to \exists a \in ran L \exists r \in (P ∖ a) H = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\}$
42	5	ad2antrr	$⊢ ((φ \land a \in ran L) \land r \in (P ∖ a)) \to G \in 𝒢_{Tarski}$
43		simplr	$⊢ ((φ \land a \in ran L) \land r \in (P ∖ a)) \to a \in ran L$
44		simpr	$⊢ ((φ \land a \in ran L) \land r \in (P ∖ a)) \to r \in (P ∖ a)$
45	1 2 3 4 42 43 44	plngval	$⊢ ((φ \land a \in ran L) \land r \in (P ∖ a)) \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))\}$
46	45	eqeq2d	$⊢ ((φ \land a \in ran L) \land r \in (P ∖ a)) \to (H = a E r \leftrightarrow H = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\})$
47	46	biimprd	$⊢ ((φ \land a \in ran L) \land r \in (P ∖ a)) \to (H = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\} \to H = a E r)$
48	47	anasss	$⊢ (φ \land (a \in ran L \land r \in (P ∖ a))) \to (H = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\} \to H = a E r)$
49	48	reximdvva	$⊢ φ \to (\exists a \in ran L \exists r \in (P ∖ a) H = \{x \in P \| (x \in a \lor x {hp}_{𝒢} (G) (a) r \lor \exists t \in a t \in (x I r))\} \to \exists a \in ran L \exists r \in (P ∖ a) H = a E r)$
50	41 49	mpd	$⊢ φ \to \exists a \in ran L \exists r \in (P ∖ a) H = a E r$

Metamath Proof Explorer

Theorem isplng

Proof