rrx2linest2

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	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\}$

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		eqid	$⊢ Y (2) - X (2) = Y (2) - X (2)$
9	1 2 3 4 6 8 7	rrx2linest	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| B p (2) = (Y (2) - X (2)) p (1) + C\}$
10		eqcom	$⊢ B p (2) = (Y (2) - X (2)) p (1) + C \leftrightarrow (Y (2) - X (2)) p (1) + C = B p (2)$
11	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
12	11	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) \in ℝ$
13	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
14	13	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) \in ℝ$
15	12 14	resubcld	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) - X (2) \in ℝ$
16	15	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to Y (2) - X (2) \in ℝ$
17	1 3	rrx2pxel	$⊢ p \in P \to p (1) \in ℝ$
18	17	adantl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to p (1) \in ℝ$
19	16 18	remulcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (Y (2) - X (2)) p (1) \in ℝ$
20	19	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (Y (2) - X (2)) p (1) \in ℂ$
21	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
22	21	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (1) \in ℝ$
23	14 22	remulcld	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) Y (1) \in ℝ$
24	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
25	24	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (1) \in ℝ$
26	25 12	remulcld	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (1) Y (2) \in ℝ$
27	23 26	resubcld	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) Y (1) - X (1) Y (2) \in ℝ$
28	7 27	eqeltrid	$⊢ (X \in P \land Y \in P \land X \neq Y) \to C \in ℝ$
29	28	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to C \in ℝ$
30	29	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to C \in ℂ$
31	22 25	resubcld	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (1) - X (1) \in ℝ$
32	6 31	eqeltrid	$⊢ (X \in P \land Y \in P \land X \neq Y) \to B \in ℝ$
33	32	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to B \in ℝ$
34	1 3	rrx2pyel	$⊢ p \in P \to p (2) \in ℝ$
35	34	adantl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to p (2) \in ℝ$
36	33 35	remulcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to B p (2) \in ℝ$
37	36	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to B p (2) \in ℂ$
38	20 30 37	addrsub	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to ((Y (2) - X (2)) p (1) + C = B p (2) \leftrightarrow C = B p (2) - (Y (2) - X (2)) p (1))$
39		eqcom	$⊢ C = B p (2) - (Y (2) - X (2)) p (1) \leftrightarrow B p (2) - (Y (2) - X (2)) p (1) = C$
40	14 12	resubcld	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) - Y (2) \in ℝ$
41	5 40	eqeltrid	$⊢ (X \in P \land Y \in P \land X \neq Y) \to A \in ℝ$
42	41	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A \in ℝ$
43	42 18	remulcld	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A p (1) \in ℝ$
44	43	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A p (1) \in ℂ$
45	44 37	addcomd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A p (1) + B p (2) = B p (2) + A p (1)$
46	12	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to Y (2) \in ℝ$
47	46	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to Y (2) \in ℂ$
48	14	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to X (2) \in ℝ$
49	48	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to X (2) \in ℂ$
50	47 49	negsubdi2d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to - (Y (2) - X (2)) = X (2) - Y (2)$
51	5 50	eqtr4id	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A = - (Y (2) - X (2))$
52	51	oveq1d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A p (1) = (- (Y (2) - X (2))) p (1)$
53	16	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to Y (2) - X (2) \in ℂ$
54	18	recnd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to p (1) \in ℂ$
55	53 54	mulneg1d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (- (Y (2) - X (2))) p (1) = - (Y (2) - X (2)) p (1)$
56	52 55	eqtrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A p (1) = - (Y (2) - X (2)) p (1)$
57	56	oveq2d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to B p (2) + A p (1) = B p (2) + (- (Y (2) - X (2)) p (1))$
58	37 20	negsubd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to B p (2) + (- (Y (2) - X (2)) p (1)) = B p (2) - (Y (2) - X (2)) p (1)$
59	45 57 58	3eqtrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to A p (1) + B p (2) = B p (2) - (Y (2) - X (2)) p (1)$
60	59	eqeq1d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (A p (1) + B p (2) = C \leftrightarrow B p (2) - (Y (2) - X (2)) p (1) = C)$
61	39 60	bitr4id	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (C = B p (2) - (Y (2) - X (2)) p (1) \leftrightarrow A p (1) + B p (2) = C)$
62	38 61	bitrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to ((Y (2) - X (2)) p (1) + C = B p (2) \leftrightarrow A p (1) + B p (2) = C)$
63	10 62	bitrid	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (B p (2) = (Y (2) - X (2)) p (1) + C \leftrightarrow A p (1) + B p (2) = C)$
64	63	rabbidva	$⊢ (X \in P \land Y \in P \land X \neq Y) \to \{p \in P \| B p (2) = (Y (2) - X (2)) p (1) + C\} = \{p \in P \| A p (1) + B p (2) = C\}$
65	9 64	eqtrd	$⊢ (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\}$

Metamath Proof Explorer

Theorem rrx2linest2

Proof