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 = ( 0 ..^ 2 )
	prelrrx2.b	|- P = ( RR ^m I )
Assertion	prelrrx2	|- ( ( A e. RR /\ B e. RR ) -> <" A B "> e. P )

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	|- I = ( 0 ..^ 2 )
2		prelrrx2.b	|- P = ( RR ^m I )
3		reex	|- RR e. _V
4	3	a1i	|- ( ( A e. RR /\ B e. RR ) -> RR e. _V )
5		simpl	|- ( ( A e. RR /\ B e. RR ) -> A e. RR )
6		simpr	|- ( ( A e. RR /\ B e. RR ) -> B e. RR )
7	4 5 6	s2mapd	|- ( ( A e. RR /\ B e. RR ) -> <" A B "> e. ( RR ^m ( 0 ..^ 2 ) ) )
8	1	oveq2i	|- ( RR ^m I ) = ( RR ^m ( 0 ..^ 2 ) )
9	2 8	eqtri	|- P = ( RR ^m ( 0 ..^ 2 ) )
10	7 9	eleqtrrdi	|- ( ( A e. RR /\ B e. RR ) -> <" A B "> e. P )