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	⊢ 𝐼 = ( 0 ..^ 2 )
	prelrrx2.b	⊢ 𝑃 = ( ℝ ↑_m 𝐼 )
	prelrrx2bd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	prelrrx2bd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion	prelrrx2bd	⊢ ( 𝜑 → ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	⊢ 𝐼 = ( 0 ..^ 2 )
2		prelrrx2.b	⊢ 𝑃 = ( ℝ ↑_m 𝐼 )
3		prelrrx2bd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		prelrrx2bd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		wrdlen2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑍 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ↔ ( ( 𝑍 ∈ Word ℝ ∧ ( ♯ ‘ 𝑍 ) = 2 ) ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ) )
6	3 4 5	syl2anc	⊢ ( 𝜑 → ( 𝑍 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ↔ ( ( 𝑍 ∈ Word ℝ ∧ ( ♯ ‘ 𝑍 ) = 2 ) ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ) )
7		s2prop	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
8	3 4 7	syl2anc	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } )
9	8	eqeq2d	⊢ ( 𝜑 → ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ↔ 𝑍 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) )
10	1	oveq2i	⊢ ( ℝ ↑_m 𝐼 ) = ( ℝ ↑_m ( 0 ..^ 2 ) )
11	2 10	eqtri	⊢ 𝑃 = ( ℝ ↑_m ( 0 ..^ 2 ) )
12	11	eleq2i	⊢ ( 𝑍 ∈ 𝑃 ↔ 𝑍 ∈ ( ℝ ↑_m ( 0 ..^ 2 ) ) )
13	12	bilani	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → 𝑍 ∈ ( ℝ ↑_m ( 0 ..^ 2 ) ) )
14	13	elmaprd	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → 𝑍 : ( 0 ..^ 2 ) ⟶ ℝ )
15		iswrdi	⊢ ( 𝑍 : ( 0 ..^ 2 ) ⟶ ℝ → 𝑍 ∈ Word ℝ )
16	14 15	syl	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → 𝑍 ∈ Word ℝ )
17		2nn0	⊢ 2 ∈ ℕ₀
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → 2 ∈ ℕ₀ )
19		fnfzo0hash	⊢ ( ( 2 ∈ ℕ₀ ∧ 𝑍 : ( 0 ..^ 2 ) ⟶ ℝ ) → ( ♯ ‘ 𝑍 ) = 2 )
20	18 14 19	syl2anc	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → ( ♯ ‘ 𝑍 ) = 2 )
21	16 20	jca	⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑃 ) → ( 𝑍 ∈ Word ℝ ∧ ( ♯ ‘ 𝑍 ) = 2 ) )
22		reex	⊢ ℝ ∈ V
23	22	a1i	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → ℝ ∈ V )
24		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → ( 0 ..^ 2 ) ∈ V )
25		simpr	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → ( ♯ ‘ 𝑍 ) = 2 )
26	25	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → 2 = ( ♯ ‘ 𝑍 ) )
27		simplr	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → 𝑍 ∈ Word ℝ )
28	26 27	wrdfd	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → 𝑍 : ( 0 ..^ 2 ) ⟶ ℝ )
29	23 24 28	elmapdd	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → 𝑍 ∈ ( ℝ ↑_m ( 0 ..^ 2 ) ) )
30	29 11	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ Word ℝ ) ∧ ( ♯ ‘ 𝑍 ) = 2 ) → 𝑍 ∈ 𝑃 )
31	30	anasss	⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ Word ℝ ∧ ( ♯ ‘ 𝑍 ) = 2 ) ) → 𝑍 ∈ 𝑃 )
32	21 31	impbida	⊢ ( 𝜑 → ( 𝑍 ∈ 𝑃 ↔ ( 𝑍 ∈ Word ℝ ∧ ( ♯ ‘ 𝑍 ) = 2 ) ) )
33	32	anbi1d	⊢ ( 𝜑 → ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ↔ ( ( 𝑍 ∈ Word ℝ ∧ ( ♯ ‘ 𝑍 ) = 2 ) ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ) )
34	6 9 33	3bitr4d	⊢ ( 𝜑 → ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ) )

Metamath Proof Explorer

Theorem prelrrx2bd

Proof