prelrrx2bd

Description: Equivalent condition for Z being a point in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by Thierry Arnoux, 10-Oct-2026)

	Ref	Expression
Hypotheses	prelrrx2.i	$⊢ I = (0 ..^2)$
	prelrrx2.b	$⊢ P = ℝ^{I}$
	prelrrx2bd.1	$⊢ φ \to A \in ℝ$
	prelrrx2bd.2	$⊢ φ \to B \in ℝ$
Assertion	prelrrx2bd	$⊢ φ \to (Z = ⟨“ A B ”⟩ \leftrightarrow (Z \in P \land (Z (0) = A \land Z (1) = B)))$

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	$⊢ I = (0 ..^2)$
2		prelrrx2.b	$⊢ P = ℝ^{I}$
3		prelrrx2bd.1	$⊢ φ \to A \in ℝ$
4		prelrrx2bd.2	$⊢ φ \to B \in ℝ$
5		wrdlen2	$⊢ (A \in ℝ \land B \in ℝ) \to (Z = \{⟨0, A⟩, ⟨1, B⟩\} \leftrightarrow ((Z \in Word ℝ \land \|Z\| = 2) \land (Z (0) = A \land Z (1) = B)))$
6	3 4 5	syl2anc	$⊢ φ \to (Z = \{⟨0, A⟩, ⟨1, B⟩\} \leftrightarrow ((Z \in Word ℝ \land \|Z\| = 2) \land (Z (0) = A \land Z (1) = B)))$
7		s2prop	$⊢ (A \in ℝ \land B \in ℝ) \to ⟨“ A B ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\}$
8	3 4 7	syl2anc	$⊢ φ \to ⟨“ A B ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\}$
9	8	eqeq2d	$⊢ φ \to (Z = ⟨“ A B ”⟩ \leftrightarrow Z = \{⟨0, A⟩, ⟨1, B⟩\})$
10	1	oveq2i	$⊢ ℝ^{I} = ℝ^{(0 ..^2)}$
11	2 10	eqtri	$⊢ P = ℝ^{(0 ..^2)}$
12	11	eleq2i	$⊢ Z \in P \leftrightarrow Z \in (ℝ^{(0 ..^2)})$
13	12	bilani	$⊢ (φ \land Z \in P) \to Z \in (ℝ^{(0 ..^2)})$
14	13	elmaprd	$⊢ (φ \land Z \in P) \to Z : (0 ..^2) ⟶ ℝ$
15		iswrdi	$⊢ Z : (0 ..^2) ⟶ ℝ \to Z \in Word ℝ$
16	14 15	syl	$⊢ (φ \land Z \in P) \to Z \in Word ℝ$
17		2nn0	$⊢ 2 \in ℕ_{0}$
18	17	a1i	$⊢ (φ \land Z \in P) \to 2 \in ℕ_{0}$
19		fnfzo0hash	$⊢ (2 \in ℕ_{0} \land Z : (0 ..^2) ⟶ ℝ) \to \|Z\| = 2$
20	18 14 19	syl2anc	$⊢ (φ \land Z \in P) \to \|Z\| = 2$
21	16 20	jca	$⊢ (φ \land Z \in P) \to (Z \in Word ℝ \land \|Z\| = 2)$
22		reex	$⊢ ℝ \in V$
23	22	a1i	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to ℝ \in V$
24		ovexd	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to (0 ..^2) \in V$
25		simpr	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to \|Z\| = 2$
26	25	eqcomd	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to 2 = \|Z\|$
27		simplr	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to Z \in Word ℝ$
28	26 27	wrdfd	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to Z : (0 ..^2) ⟶ ℝ$
29	23 24 28	elmapdd	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to Z \in (ℝ^{(0 ..^2)})$
30	29 11	eleqtrrdi	$⊢ ((φ \land Z \in Word ℝ) \land \|Z\| = 2) \to Z \in P$
31	30	anasss	$⊢ (φ \land (Z \in Word ℝ \land \|Z\| = 2)) \to Z \in P$
32	21 31	impbida	$⊢ φ \to (Z \in P \leftrightarrow (Z \in Word ℝ \land \|Z\| = 2))$
33	32	anbi1d	$⊢ φ \to ((Z \in P \land (Z (0) = A \land Z (1) = B)) \leftrightarrow ((Z \in Word ℝ \land \|Z\| = 2) \land (Z (0) = A \land Z (1) = B)))$
34	6 9 33	3bitr4d	$⊢ φ \to (Z = ⟨“ A B ”⟩ \leftrightarrow (Z \in P \land (Z (0) = A \land Z (1) = B)))$

Metamath Proof Explorer

Theorem prelrrx2bd

Proof