Metamath Proof Explorer

Theorem rrx2pnedifcoorneor

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

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

Proof

Step Hyp Ref Expression
1 rrx2pnecoorneor.i 
 |-  I = { 1 , 2 }
2 rrx2pnecoorneor.b 
 |-  P = ( RR ^m I )
3 rrx2pnedifcoorneor.a 
 |-  A = ( ( Y ` 1 ) - ( X ` 1 ) )
4 rrx2pnedifcoorneor.b 
 |-  B = ( ( Y ` 2 ) - ( X ` 2 ) )
5 1 2 rrx2pnecoorneor 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) )
6 3 neeq1i 
 |-  ( A =/= 0 <-> ( ( Y ` 1 ) - ( X ` 1 ) ) =/= 0 )
7 4 neeq1i 
 |-  ( B =/= 0 <-> ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 )
8 6 7 orbi12i 
 |-  ( ( A =/= 0 \/ B =/= 0 ) <-> ( ( ( Y ` 1 ) - ( X ` 1 ) ) =/= 0 \/ ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 ) )
9 1 2 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
10 9 recnd 
 |-  ( Y e. P -> ( Y ` 1 ) e. CC )
11 1 2 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
12 11 recnd 
 |-  ( X e. P -> ( X ` 1 ) e. CC )
13 subeq0 
 |-  ( ( ( Y ` 1 ) e. CC /\ ( X ` 1 ) e. CC ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) = 0 <-> ( Y ` 1 ) = ( X ` 1 ) ) )
14 10 12 13 syl2anr 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) = 0 <-> ( Y ` 1 ) = ( X ` 1 ) ) )
15 14 necon3bid 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( Y ` 1 ) - ( X ` 1 ) ) =/= 0 <-> ( Y ` 1 ) =/= ( X ` 1 ) ) )
16 1 2 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
17 16 recnd 
 |-  ( Y e. P -> ( Y ` 2 ) e. CC )
18 1 2 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
19 18 recnd 
 |-  ( X e. P -> ( X ` 2 ) e. CC )
20 subeq0 
 |-  ( ( ( Y ` 2 ) e. CC /\ ( X ` 2 ) e. CC ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) = 0 <-> ( Y ` 2 ) = ( X ` 2 ) ) )
21 17 19 20 syl2anr 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) = 0 <-> ( Y ` 2 ) = ( X ` 2 ) ) )
22 21 necon3bid 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 <-> ( Y ` 2 ) =/= ( X ` 2 ) ) )
23 15 22 orbi12d 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) =/= 0 \/ ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 ) <-> ( ( Y ` 1 ) =/= ( X ` 1 ) \/ ( Y ` 2 ) =/= ( X ` 2 ) ) ) )
24 necom 
 |-  ( ( Y ` 1 ) =/= ( X ` 1 ) <-> ( X ` 1 ) =/= ( Y ` 1 ) )
25 necom 
 |-  ( ( Y ` 2 ) =/= ( X ` 2 ) <-> ( X ` 2 ) =/= ( Y ` 2 ) )
26 24 25 orbi12i 
 |-  ( ( ( Y ` 1 ) =/= ( X ` 1 ) \/ ( Y ` 2 ) =/= ( X ` 2 ) ) <-> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) )
27 23 26 bitrdi 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( ( Y ` 1 ) - ( X ` 1 ) ) =/= 0 \/ ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 ) <-> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) ) )
28 8 27 syl5bb 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) ) )
29 28 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( ( X ` 1 ) =/= ( Y ` 1 ) \/ ( X ` 2 ) =/= ( Y ` 2 ) ) ) )
30 5 29 mpbird 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A =/= 0 \/ B =/= 0 ) )