Metamath Proof Explorer


Theorem rrx2pnedifcoorneorr

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 = I
rrx2pnedifcoorneor.a A = Y 1 X 1
rrx2pnedifcoorneorr.b B = X 2 Y 2
Assertion rrx2pnedifcoorneorr X P Y P X Y A 0 B 0

Proof

Step Hyp Ref Expression
1 rrx2pnecoorneor.i I = 1 2
2 rrx2pnecoorneor.b P = I
3 rrx2pnedifcoorneor.a A = Y 1 X 1
4 rrx2pnedifcoorneorr.b B = X 2 Y 2
5 eqid Y 2 X 2 = Y 2 X 2
6 1 2 3 5 rrx2pnedifcoorneor X P Y P X Y A 0 Y 2 X 2 0
7 eqcom Y 2 = X 2 X 2 = Y 2
8 7 a1i X P Y P X Y Y 2 = X 2 X 2 = Y 2
9 1 2 rrx2pyel X P X 2
10 9 recnd X P X 2
11 1 2 rrx2pyel Y P Y 2
12 11 recnd Y P Y 2
13 10 12 anim12i X P Y P X 2 Y 2
14 13 ancomd X P Y P Y 2 X 2
15 14 3adant3 X P Y P X Y Y 2 X 2
16 subeq0 Y 2 X 2 Y 2 X 2 = 0 Y 2 = X 2
17 15 16 syl X P Y P X Y Y 2 X 2 = 0 Y 2 = X 2
18 13 3adant3 X P Y P X Y X 2 Y 2
19 subeq0 X 2 Y 2 X 2 Y 2 = 0 X 2 = Y 2
20 18 19 syl X P Y P X Y X 2 Y 2 = 0 X 2 = Y 2
21 8 17 20 3bitr4d X P Y P X Y Y 2 X 2 = 0 X 2 Y 2 = 0
22 4 eqcomi X 2 Y 2 = B
23 22 eqeq1i X 2 Y 2 = 0 B = 0
24 21 23 bitrdi X P Y P X Y Y 2 X 2 = 0 B = 0
25 24 necon3bid X P Y P X Y Y 2 X 2 0 B 0
26 25 orbi2d X P Y P X Y A 0 Y 2 X 2 0 A 0 B 0
27 6 26 mpbid X P Y P X Y A 0 B 0