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 \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 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 \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor Y (2) - X (2) \neq 0)$
7		eqcom	$⊢ Y (2) = X (2) \leftrightarrow X (2) = Y (2)$
8	7	a1i	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (2) = X (2) \leftrightarrow X (2) = Y (2))$
9	1 2	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
10	9	recnd	$⊢ X \in P \to X (2) \in ℂ$
11	1 2	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
12	11	recnd	$⊢ Y \in P \to Y (2) \in ℂ$
13	10 12	anim12i	$⊢ (X \in P \land Y \in P) \to (X (2) \in ℂ \land Y (2) \in ℂ)$
14	13	ancomd	$⊢ (X \in P \land Y \in P) \to (Y (2) \in ℂ \land X (2) \in ℂ)$
15	14	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (2) \in ℂ \land X (2) \in ℂ)$
16		subeq0	$⊢ (Y (2) \in ℂ \land X (2) \in ℂ) \to (Y (2) - X (2) = 0 \leftrightarrow Y (2) = X (2))$
17	15 16	syl	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (2) - X (2) = 0 \leftrightarrow Y (2) = X (2))$
18	13	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (2) \in ℂ \land Y (2) \in ℂ)$
19		subeq0	$⊢ (X (2) \in ℂ \land Y (2) \in ℂ) \to (X (2) - Y (2) = 0 \leftrightarrow X (2) = Y (2))$
20	18 19	syl	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (2) - Y (2) = 0 \leftrightarrow X (2) = Y (2))$
21	8 17 20	3bitr4d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (2) - X (2) = 0 \leftrightarrow X (2) - Y (2) = 0)$
22	4	eqcomi	$⊢ X (2) - Y (2) = B$
23	22	eqeq1i	$⊢ X (2) - Y (2) = 0 \leftrightarrow B = 0$
24	21 23	bitrdi	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (2) - X (2) = 0 \leftrightarrow B = 0)$
25	24	necon3bid	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (2) - X (2) \neq 0 \leftrightarrow B \neq 0)$
26	25	orbi2d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to ((A \neq 0 \lor Y (2) - X (2) \neq 0) \leftrightarrow (A \neq 0 \lor B \neq 0))$
27	6 26	mpbid	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 0)$

Metamath Proof Explorer

Theorem rrx2pnedifcoorneorr

Proof