Metamath Proof Explorer

Theorem elrrx2linest2

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2 in another "standard form" (usually with ( p1 ) = x and ( p2 ) = y ). (Contributed by AV, 23-Feb-2023)

		Ref	Expression
	Hypotheses	rrx2linest2.i	$⊢ I = \{1, 2\}$
		rrx2linest2.e	$⊢ E = I$
		rrx2linest2.p	$⊢ P = ℝ^{I}$
		rrx2linest2.l	$⊢ L = {Line}_{M} (E)$
		rrx2linest2.a	$⊢ A = X (2) - Y (2)$
		rrx2linest2.b	$⊢ B = Y (1) - X (1)$
		rrx2linest2.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
	Assertion	elrrx2linest2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (G \in (X L Y) \leftrightarrow (G \in P \land A G (1) + B G (2) = C))$

Proof

Step	Hyp	Ref	Expression
1		rrx2linest2.i	$⊢ I = \{1, 2\}$
2		rrx2linest2.e	$⊢ E = I$
3		rrx2linest2.p	$⊢ P = ℝ^{I}$
4		rrx2linest2.l	$⊢ L = {Line}_{M} (E)$
5		rrx2linest2.a	$⊢ A = X (2) - Y (2)$
6		rrx2linest2.b	$⊢ B = Y (1) - X (1)$
7		rrx2linest2.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
8	1 2 3 4 5 6 7	rrx2linest2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| A p (1) + B p (2) = C\}$
9	8	eleq2d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (G \in (X L Y) \leftrightarrow G \in \{p \in P \| A p (1) + B p (2) = C\})$
10		fveq1	$⊢ p = G \to p (1) = G (1)$
11	10	oveq2d	$⊢ p = G \to A p (1) = A G (1)$
12		fveq1	$⊢ p = G \to p (2) = G (2)$
13	12	oveq2d	$⊢ p = G \to B p (2) = B G (2)$
14	11 13	oveq12d	$⊢ p = G \to A p (1) + B p (2) = A G (1) + B G (2)$
15	14	eqeq1d	$⊢ p = G \to (A p (1) + B p (2) = C \leftrightarrow A G (1) + B G (2) = C)$
16	15	elrab	$⊢ G \in \{p \in P \| A p (1) + B p (2) = C\} \leftrightarrow (G \in P \land A G (1) + B G (2) = C)$
17	9 16	bitrdi	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (G \in (X L Y) \leftrightarrow (G \in P \land A G (1) + B G (2) = C))$