Metamath Proof Explorer

Theorem rrx2pnecoorneor

Description: If two different points X and Y in a real Euclidean space of dimension 2 are different, then they are different at least at one coordinate. (Contributed by AV, 26-Feb-2023)

Ref Expression
Hypotheses rrx2pnecoorneor.i 
|- I = ( 0 ..^ 2 )
rrx2pnecoorneor.b 
|- P = ( RR ^m I )
Assertion rrx2pnecoorneor 
|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 0 ) =/= ( Y ` 0 ) \/ ( X ` 1 ) =/= ( Y ` 1 ) ) )

Proof

Step Hyp Ref Expression
1 rrx2pnecoorneor.i 
 |-  I = ( 0 ..^ 2 )
2 rrx2pnecoorneor.b 
 |-  P = ( RR ^m I )
3 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
4 1 3 eqtri 
 |-  I = { 0 , 1 }
5 4 raleqi 
 |-  ( A. i e. I ( X ` i ) = ( Y ` i ) <-> A. i e. { 0 , 1 } ( X ` i ) = ( Y ` i ) )
6 c0ex 
 |-  0 e. _V
7 1ex 
 |-  1 e. _V
8 fveq2 
 |-  ( i = 0 -> ( X ` i ) = ( X ` 0 ) )
9 fveq2 
 |-  ( i = 0 -> ( Y ` i ) = ( Y ` 0 ) )
10 8 9 eqeq12d 
 |-  ( i = 0 -> ( ( X ` i ) = ( Y ` i ) <-> ( X ` 0 ) = ( Y ` 0 ) ) )
11 fveq2 
 |-  ( i = 1 -> ( X ` i ) = ( X ` 1 ) )
12 fveq2 
 |-  ( i = 1 -> ( Y ` i ) = ( Y ` 1 ) )
13 11 12 eqeq12d 
 |-  ( i = 1 -> ( ( X ` i ) = ( Y ` i ) <-> ( X ` 1 ) = ( Y ` 1 ) ) )
14 6 7 10 13 ralpr 
 |-  ( A. i e. { 0 , 1 } ( X ` i ) = ( Y ` i ) <-> ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) )
15 5 14 bitri 
 |-  ( A. i e. I ( X ` i ) = ( Y ` i ) <-> ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) )
16 15 bilanri 
 |-  ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) ) -> A. i e. I ( X ` i ) = ( Y ` i ) )
17 elmapfn 
 |-  ( X e. ( RR ^m I ) -> X Fn I )
18 17 2 eleq2s 
 |-  ( X e. P -> X Fn I )
19 elmapfn 
 |-  ( Y e. ( RR ^m I ) -> Y Fn I )
20 19 2 eleq2s 
 |-  ( Y e. P -> Y Fn I )
21 18 20 anim12i 
 |-  ( ( X e. P /\ Y e. P ) -> ( X Fn I /\ Y Fn I ) )
22 21 adantr 
 |-  ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) ) -> ( X Fn I /\ Y Fn I ) )
23 eqfnfv 
 |-  ( ( X Fn I /\ Y Fn I ) -> ( X = Y <-> A. i e. I ( X ` i ) = ( Y ` i ) ) )
24 22 23 syl 
 |-  ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) ) -> ( X = Y <-> A. i e. I ( X ` i ) = ( Y ` i ) ) )
25 16 24 mpbird 
 |-  ( ( ( X e. P /\ Y e. P ) /\ ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) ) -> X = Y )
26 25 ex 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) -> X = Y ) )
27 26 necon3ad 
 |-  ( ( X e. P /\ Y e. P ) -> ( X =/= Y -> -. ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) ) )
28 27 3impia 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> -. ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) )
29 neorian 
 |-  ( ( ( X ` 0 ) =/= ( Y ` 0 ) \/ ( X ` 1 ) =/= ( Y ` 1 ) ) <-> -. ( ( X ` 0 ) = ( Y ` 0 ) /\ ( X ` 1 ) = ( Y ` 1 ) ) )
30 28 29 sylibr 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 0 ) =/= ( Y ` 0 ) \/ ( X ` 1 ) =/= ( Y ` 1 ) ) )