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

Proof

Step	Hyp	Ref	Expression
1		rrx2pnecoorneor.i	⊢ 𝐼 = { 1 , 2 }
2		rrx2pnecoorneor.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		rrx2pnedifcoorneor.a	⊢ 𝐴 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
4		rrx2pnedifcoorneor.b	⊢ 𝐵 = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) )
5	1 2	rrx2pnecoorneor	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )
6	3	neeq1i	⊢ ( 𝐴 ≠ 0 ↔ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ≠ 0 )
7	4	neeq1i	⊢ ( 𝐵 ≠ 0 ↔ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 )
8	6 7	orbi12i	⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ≠ 0 ∨ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ) )
9	1 2	rrx2pxel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
10	9	recnd	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℂ )
11	1 2	rrx2pxel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
12	11	recnd	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℂ )
13		subeq0	⊢ ( ( ( 𝑌 ‘ 1 ) ∈ ℂ ∧ ( 𝑋 ‘ 1 ) ∈ ℂ ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 0 ↔ ( 𝑌 ‘ 1 ) = ( 𝑋 ‘ 1 ) ) )
14	10 12 13	syl2anr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = 0 ↔ ( 𝑌 ‘ 1 ) = ( 𝑋 ‘ 1 ) ) )
15	14	necon3bid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ≠ 0 ↔ ( 𝑌 ‘ 1 ) ≠ ( 𝑋 ‘ 1 ) ) )
16	1 2	rrx2pyel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
17	16	recnd	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℂ )
18	1 2	rrx2pyel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
19	18	recnd	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℂ )
20		subeq0	⊢ ( ( ( 𝑌 ‘ 2 ) ∈ ℂ ∧ ( 𝑋 ‘ 2 ) ∈ ℂ ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ) )
21	17 19 20	syl2anr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ) )
22	21	necon3bid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ↔ ( 𝑌 ‘ 2 ) ≠ ( 𝑋 ‘ 2 ) ) )
23	15 22	orbi12d	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ≠ 0 ∨ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ) ↔ ( ( 𝑌 ‘ 1 ) ≠ ( 𝑋 ‘ 1 ) ∨ ( 𝑌 ‘ 2 ) ≠ ( 𝑋 ‘ 2 ) ) ) )
24		necom	⊢ ( ( 𝑌 ‘ 1 ) ≠ ( 𝑋 ‘ 1 ) ↔ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
25		necom	⊢ ( ( 𝑌 ‘ 2 ) ≠ ( 𝑋 ‘ 2 ) ↔ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) )
26	24 25	orbi12i	⊢ ( ( ( 𝑌 ‘ 1 ) ≠ ( 𝑋 ‘ 1 ) ∨ ( 𝑌 ‘ 2 ) ≠ ( 𝑋 ‘ 2 ) ) ↔ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )
27	23 26	bitrdi	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ≠ 0 ∨ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ) ↔ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) )
28	8 27	syl5bb	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) )
29	28	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) )
30	5 29	mpbird	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )