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=12
rrx2pnecoorneor.b P=I
rrx2pnedifcoorneor.a A=Y1X1
rrx2pnedifcoorneorr.b B=X2Y2
Assertion rrx2pnedifcoorneorr XPYPXYA0B0

Proof

Step Hyp Ref Expression
1 rrx2pnecoorneor.i I=12
2 rrx2pnecoorneor.b P=I
3 rrx2pnedifcoorneor.a A=Y1X1
4 rrx2pnedifcoorneorr.b B=X2Y2
5 eqid Y2X2=Y2X2
6 1 2 3 5 rrx2pnedifcoorneor XPYPXYA0Y2X20
7 eqcom Y2=X2X2=Y2
8 7 a1i XPYPXYY2=X2X2=Y2
9 1 2 rrx2pyel XPX2
10 9 recnd XPX2
11 1 2 rrx2pyel YPY2
12 11 recnd YPY2
13 10 12 anim12i XPYPX2Y2
14 13 ancomd XPYPY2X2
15 14 3adant3 XPYPXYY2X2
16 subeq0 Y2X2Y2X2=0Y2=X2
17 15 16 syl XPYPXYY2X2=0Y2=X2
18 13 3adant3 XPYPXYX2Y2
19 subeq0 X2Y2X2Y2=0X2=Y2
20 18 19 syl XPYPXYX2Y2=0X2=Y2
21 8 17 20 3bitr4d XPYPXYY2X2=0X2Y2=0
22 4 eqcomi X2Y2=B
23 22 eqeq1i X2Y2=0B=0
24 21 23 bitrdi XPYPXYY2X2=0B=0
25 24 necon3bid XPYPXYY2X20B0
26 25 orbi2d XPYPXYA0Y2X20A0B0
27 6 26 mpbid XPYPXYA0B0