Metamath Proof Explorer

Theorem prelrrx2b

Description: Equivalent condition for being one of a pair of points in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023)

Ref Expression
Hypotheses prelrrx2.i 
|- I = ( 0 ..^ 2 )
prelrrx2.b 
|- P = ( RR ^m I )
Assertion prelrrx2b 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z e. P /\ ( ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) \/ ( ( Z ` 0 ) = X /\ ( Z ` 1 ) = Y ) ) ) <-> Z e. { <" A B "> , <" X Y "> } ) )

Proof

Step Hyp Ref Expression
1 prelrrx2.i 
 |-  I = ( 0 ..^ 2 )
2 prelrrx2.b 
 |-  P = ( RR ^m I )
3 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> A e. RR )
4 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> B e. RR )
5 3 4 s2cld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> <" A B "> e. Word RR )
6 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> X e. RR )
7 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> Y e. RR )
8 6 7 s2cld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> <" X Y "> e. Word RR )
9 elpr2g 
 |-  ( ( <" A B "> e. Word RR /\ <" X Y "> e. Word RR ) -> ( Z e. { <" A B "> , <" X Y "> } <-> ( Z = <" A B "> \/ Z = <" X Y "> ) ) )
10 5 8 9 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z e. { <" A B "> , <" X Y "> } <-> ( Z = <" A B "> \/ Z = <" X Y "> ) ) )
11 1 2 3 4 prelrrx2bd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z = <" A B "> <-> ( Z e. P /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) ) )
12 1 2 6 7 prelrrx2bd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z = <" X Y "> <-> ( Z e. P /\ ( ( Z ` 0 ) = X /\ ( Z ` 1 ) = Y ) ) ) )
13 11 12 orbi12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z = <" A B "> \/ Z = <" X Y "> ) <-> ( ( Z e. P /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) \/ ( Z e. P /\ ( ( Z ` 0 ) = X /\ ( Z ` 1 ) = Y ) ) ) ) )
14 andi 
 |-  ( ( Z e. P /\ ( ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) \/ ( ( Z ` 0 ) = X /\ ( Z ` 1 ) = Y ) ) ) <-> ( ( Z e. P /\ ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) ) \/ ( Z e. P /\ ( ( Z ` 0 ) = X /\ ( Z ` 1 ) = Y ) ) ) )
15 13 14 bitr4di 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z = <" A B "> \/ Z = <" X Y "> ) <-> ( Z e. P /\ ( ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) \/ ( ( Z ` 0 ) = X /\ ( Z ` 1 ) = Y ) ) ) ) )
16 10 15 bitr2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z e. P /\ ( ( ( Z ` 0 ) = A /\ ( Z ` 1 ) = B ) \/ ( ( Z ` 0 ) = X /\ ( Z ` 1 ) = Y ) ) ) <-> Z e. { <" A B "> , <" X Y "> } ) )