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 𝐼 = { 1 , 2 }
rrx2pnecoorneor.b 𝑃 = ( ℝ ↑m 𝐼 )
rrx2pnedifcoorneor.a 𝐴 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
rrx2pnedifcoorneorr.b 𝐵 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
Assertion rrx2pnedifcoorneorr ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )

Proof

Step Hyp Ref Expression
1 rrx2pnecoorneor.i 𝐼 = { 1 , 2 }
2 rrx2pnecoorneor.b 𝑃 = ( ℝ ↑m 𝐼 )
3 rrx2pnedifcoorneor.a 𝐴 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
4 rrx2pnedifcoorneorr.b 𝐵 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
5 eqid ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
6 1 2 3 5 rrx2pnedifcoorneor ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝐴 ≠ 0 ∨ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ) )
7 eqcom ( ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) )
8 7 a1i ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
9 1 2 rrx2pyel ( 𝑋𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
10 9 recnd ( 𝑋𝑃 → ( 𝑋 ‘ 2 ) ∈ ℂ )
11 1 2 rrx2pyel ( 𝑌𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
12 11 recnd ( 𝑌𝑃 → ( 𝑌 ‘ 2 ) ∈ ℂ )
13 10 12 anim12i ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑋 ‘ 2 ) ∈ ℂ ∧ ( 𝑌 ‘ 2 ) ∈ ℂ ) )
14 13 ancomd ( ( 𝑋𝑃𝑌𝑃 ) → ( ( 𝑌 ‘ 2 ) ∈ ℂ ∧ ( 𝑋 ‘ 2 ) ∈ ℂ ) )
15 14 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝑌 ‘ 2 ) ∈ ℂ ∧ ( 𝑋 ‘ 2 ) ∈ ℂ ) )
16 subeq0 ( ( ( 𝑌 ‘ 2 ) ∈ ℂ ∧ ( 𝑋 ‘ 2 ) ∈ ℂ ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ) )
17 15 16 syl ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ) )
18 13 3adant3 ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝑋 ‘ 2 ) ∈ ℂ ∧ ( 𝑌 ‘ 2 ) ∈ ℂ ) )
19 subeq0 ( ( ( 𝑋 ‘ 2 ) ∈ ℂ ∧ ( 𝑌 ‘ 2 ) ∈ ℂ ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
20 18 19 syl ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
21 8 17 20 3bitr4d ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ) )
22 4 eqcomi ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 𝐵
23 22 eqeq1i ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ↔ 𝐵 = 0 )
24 21 23 bitrdi ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ 𝐵 = 0 ) )
25 24 necon3bid ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ↔ 𝐵 ≠ 0 ) )
26 25 orbi2d ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( ( 𝐴 ≠ 0 ∨ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ) ↔ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) )
27 6 26 mpbid ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )