Metamath Proof Explorer

Theorem 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 = ( RR ^m I )
prelrrx2bd.1 
|- ( ph -> A e. RR )
prelrrx2bd.2 
|- ( ph -> B e. RR )
Assertion prelrrx2bd 
|- ( ph -> ( Z = <" A B "> <-> ( Z e. P /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) ) )

Proof

Step Hyp Ref Expression
1 prelrrx2.i 
 |-  I = ( 0 ..^ 2 )
2 prelrrx2.b 
 |-  P = ( RR ^m I )
3 prelrrx2bd.1 
 |-  ( ph -> A e. RR )
4 prelrrx2bd.2 
 |-  ( ph -> B e. RR )
5 wrdlen2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( Z = { <. 0 , A >. , <. 1 , B >. } <-> ( ( Z e. Word RR /\ ( # ` Z ) = 2 ) /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) ) )
6 3 4 5 syl2anc 
 |-  ( ph -> ( Z = { <. 0 , A >. , <. 1 , B >. } <-> ( ( Z e. Word RR /\ ( # ` Z ) = 2 ) /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) ) )
7 s2prop 
 |-  ( ( A e. RR /\ B e. RR ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
8 3 4 7 syl2anc 
 |-  ( ph -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
9 8 eqeq2d 
 |-  ( ph -> ( Z = <" A B "> <-> Z = { <. 0 , A >. , <. 1 , B >. } ) )
10 1 oveq2i 
 |-  ( RR ^m I ) = ( RR ^m ( 0 ..^ 2 ) )
11 2 10 eqtri 
 |-  P = ( RR ^m ( 0 ..^ 2 ) )
12 11 eleq2i 
 |-  ( Z e. P <-> Z e. ( RR ^m ( 0 ..^ 2 ) ) )
13 12 bilani 
 |-  ( ( ph /\ Z e. P ) -> Z e. ( RR ^m ( 0 ..^ 2 ) ) )
14 13 elmaprd 
 |-  ( ( ph /\ Z e. P ) -> Z : ( 0 ..^ 2 ) --> RR )
15 iswrdi 
 |-  ( Z : ( 0 ..^ 2 ) --> RR -> Z e. Word RR )
16 14 15 syl 
 |-  ( ( ph /\ Z e. P ) -> Z e. Word RR )
17 2nn0 
 |-  2 e. NN0
18 17 a1i 
 |-  ( ( ph /\ Z e. P ) -> 2 e. NN0 )
19 fnfzo0hash 
 |-  ( ( 2 e. NN0 /\ Z : ( 0 ..^ 2 ) --> RR ) -> ( # ` Z ) = 2 )
20 18 14 19 syl2anc 
 |-  ( ( ph /\ Z e. P ) -> ( # ` Z ) = 2 )
21 16 20 jca 
 |-  ( ( ph /\ Z e. P ) -> ( Z e. Word RR /\ ( # ` Z ) = 2 ) )
22 reex 
 |-  RR e. _V
23 22 a1i 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> RR e. _V )
24 ovexd 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> ( 0 ..^ 2 ) e. _V )
25 simpr 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> ( # ` Z ) = 2 )
26 25 eqcomd 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> 2 = ( # ` Z ) )
27 simplr 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> Z e. Word RR )
28 26 27 wrdfd 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> Z : ( 0 ..^ 2 ) --> RR )
29 23 24 28 elmapdd 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> Z e. ( RR ^m ( 0 ..^ 2 ) ) )
30 29 11 eleqtrrdi 
 |-  ( ( ( ph /\ Z e. Word RR ) /\ ( # ` Z ) = 2 ) -> Z e. P )
31 30 anasss 
 |-  ( ( ph /\ ( Z e. Word RR /\ ( # ` Z ) = 2 ) ) -> Z e. P )
32 21 31 impbida 
 |-  ( ph -> ( Z e. P <-> ( Z e. Word RR /\ ( # ` Z ) = 2 ) ) )
33 32 anbi1d 
 |-  ( ph -> ( ( Z e. P /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) <-> ( ( Z e. Word RR /\ ( # ` Z ) = 2 ) /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) ) )
34 6 9 33 3bitr4d 
 |-  ( ph -> ( Z = <" A B "> <-> ( Z e. P /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) ) )