Theorem prelrrx2

Description: A doubleton word of real numbers is a point in a real Euclidean space of dimension 2. (Contributed by AV, 4-Feb-2023)

	Ref	Expression
Hypotheses	prelrrx2.i	$$⊢I=\left(0..^2\right)$$
	prelrrx2.b	$$⊢P={ℝ}^I$$
Assertion	prelrrx2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to ⟨“AB”⟩\in P$$

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	$$⊢I=\left(0..^2\right)$$
2		prelrrx2.b	$$⊢P={ℝ}^I$$
3		reex	$$⊢ℝ\in \mathrm{V}$$
4	3	a1i	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to ℝ\in \mathrm{V}$$
5		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
6		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
7	4 5 6	s2mapd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to ⟨“AB”⟩\in \left({ℝ}^{\left(0..^2\right)}\right)$$
8	1	oveq2i	$$⊢{ℝ}^I={ℝ}^{\left(0..^2\right)}$$
9	2 8	eqtri	$$⊢P={ℝ}^{\left(0..^2\right)}$$
10	7 9	eleqtrrdi	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to ⟨“AB”⟩\in P$$