line2

Description: Example for a line G passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023)

	Ref	Expression
Hypotheses	line2.i	$⊢ I = \{1, 2\}$
	line2.e	$⊢ E = I$
	line2.p	$⊢ P = ℝ^{I}$
	line2.l	$⊢ L = {Line}_{M} (E)$
	line2.g	$⊢ G = \{p \in P \| A p (1) + B p (2) = C\}$
	line2.x	$⊢ X = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\}$
	line2.y	$⊢ Y = \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\}$
Assertion	line2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to G = X L Y$

Proof

Step	Hyp	Ref	Expression
1		line2.i	$⊢ I = \{1, 2\}$
2		line2.e	$⊢ E = I$
3		line2.p	$⊢ P = ℝ^{I}$
4		line2.l	$⊢ L = {Line}_{M} (E)$
5		line2.g	$⊢ G = \{p \in P \| A p (1) + B p (2) = C\}$
6		line2.x	$⊢ X = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\}$
7		line2.y	$⊢ Y = \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\}$
8		simp1	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to A \in ℝ$
9	8	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to A \in ℝ$
10	1 3	rrx2pxel	$⊢ p \in P \to p (1) \in ℝ$
11	10	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to p (1) \in ℝ$
12	9 11	remulcld	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to A p (1) \in ℝ$
13	12	recnd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to A p (1) \in ℂ$
14		simpl2l	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to B \in ℝ$
15	1 3	rrx2pyel	$⊢ p \in P \to p (2) \in ℝ$
16	15	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to p (2) \in ℝ$
17	14 16	remulcld	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to B p (2) \in ℝ$
18	17	recnd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to B p (2) \in ℂ$
19		simpl	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℝ$
20	19	recnd	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℂ$
21	20	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \in ℂ$
22	21	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to B \in ℂ$
23		simp2r	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \neq 0$
24	23	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to B \neq 0$
25	13 18 22 24	divdird	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{A p (1) + B p (2)}{B} = (\frac{A p (1)}{B}) + (\frac{B p (2)}{B})$
26	15	recnd	$⊢ p \in P \to p (2) \in ℂ$
27	26	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to p (2) \in ℂ$
28	27 22 24	divcan3d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{B p (2)}{B} = p (2)$
29	28	oveq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{A p (1)}{B}) + (\frac{B p (2)}{B}) = (\frac{A p (1)}{B}) + p (2)$
30	25 29	eqtrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{A p (1) + B p (2)}{B} = (\frac{A p (1)}{B}) + p (2)$
31	30	eqeq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{A p (1) + B p (2)}{B} = \frac{C}{B} \leftrightarrow (\frac{A p (1)}{B}) + p (2) = \frac{C}{B})$
32	12 14 24	redivcld	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{A p (1)}{B} \in ℝ$
33	32	recnd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{A p (1)}{B} \in ℂ$
34		simp3	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℝ$
35	19	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \in ℝ$
36	34 35 23	redivcld	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{C}{B} \in ℝ$
37	36	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{C}{B} \in ℂ$
38	37	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{C}{B} \in ℂ$
39	33 27 38	addrsub	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to ((\frac{A p (1)}{B}) + p (2) = \frac{C}{B} \leftrightarrow p (2) = (\frac{C}{B}) - (\frac{A p (1)}{B}))$
40		simpl3	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to C \in ℝ$
41	40 14 24	redivcld	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{C}{B} \in ℝ$
42	41	recnd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{C}{B} \in ℂ$
43	33 42	negsubdi2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - ((\frac{A p (1)}{B}) - (\frac{C}{B})) = (\frac{C}{B}) - (\frac{A p (1)}{B})$
44	33 42	negsubdid	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - ((\frac{A p (1)}{B}) - (\frac{C}{B})) = - (\frac{A p (1)}{B}) + (\frac{C}{B})$
45	43 44	eqtr3d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{C}{B}) - (\frac{A p (1)}{B}) = - (\frac{A p (1)}{B}) + (\frac{C}{B})$
46	45	eqeq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (p (2) = (\frac{C}{B}) - (\frac{A p (1)}{B}) \leftrightarrow p (2) = - (\frac{A p (1)}{B}) + (\frac{C}{B}))$
47	31 39 46	3bitrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{A p (1) + B p (2)}{B} = \frac{C}{B} \leftrightarrow p (2) = - (\frac{A p (1)}{B}) + (\frac{C}{B}))$
48	12 17	readdcld	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to A p (1) + B p (2) \in ℝ$
49	48	recnd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to A p (1) + B p (2) \in ℂ$
50	34	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℂ$
51	50	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to C \in ℂ$
52		recn	$⊢ B \in ℝ \to B \in ℂ$
53	52	anim1i	$⊢ (B \in ℝ \land B \neq 0) \to (B \in ℂ \land B \neq 0)$
54	53	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (B \in ℂ \land B \neq 0)$
55	54	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (B \in ℂ \land B \neq 0)$
56		div11	$⊢ (A p (1) + B p (2) \in ℂ \land C \in ℂ \land (B \in ℂ \land B \neq 0)) \to (\frac{A p (1) + B p (2)}{B} = \frac{C}{B} \leftrightarrow A p (1) + B p (2) = C)$
57	49 51 55 56	syl3anc	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{A p (1) + B p (2)}{B} = \frac{C}{B} \leftrightarrow A p (1) + B p (2) = C)$
58	13 22 24	divnegd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - \frac{A p (1)}{B} = \frac{- A p (1)}{B}$
59	8	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to A \in ℂ$
60	59	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to A \in ℂ$
61	10	recnd	$⊢ p \in P \to p (1) \in ℂ$
62	61	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to p (1) \in ℂ$
63	60 62	mulneg1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (- A) p (1) = - A p (1)$
64	63	eqcomd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - A p (1) = (- A) p (1)$
65	64	oveq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{- A p (1)}{B} = \frac{(- A) p (1)}{B}$
66	58 65	eqtrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - \frac{A p (1)}{B} = \frac{(- A) p (1)}{B}$
67		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
68	67	recnd	$⊢ A \in ℝ \to - A \in ℂ$
69	68	3ad2ant1	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to - A \in ℂ$
70	69	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - A \in ℂ$
71		div23	$⊢ (- A \in ℂ \land p (1) \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{(- A) p (1)}{B} = (\frac{- A}{B}) p (1)$
72	70 62 55 71	syl3anc	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{(- A) p (1)}{B} = (\frac{- A}{B}) p (1)$
73	6	fveq1i	$⊢ X (1) = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1)$
74		1ex	$⊢ 1 \in V$
75		c0ex	$⊢ 0 \in V$
76		1ne2	$⊢ 1 \neq 2$
77	74 75 76	3pm3.2i	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2)$
78		fvpr1g	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
79	77 78	mp1i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
80	73 79	syl5eq	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X (1) = 0$
81	80	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to X (1) = 0$
82	81	oveq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to p (1) - X (1) = p (1) - 0$
83	62	subid1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to p (1) - 0 = p (1)$
84	82 83	eqtr2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to p (1) = p (1) - X (1)$
85	84	oveq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{- A}{B}) p (1) = (\frac{- A}{B}) (p (1) - X (1))$
86	66 72 85	3eqtrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - \frac{A p (1)}{B} = (\frac{- A}{B}) (p (1) - X (1))$
87	86	oveq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to - (\frac{A p (1)}{B}) + (\frac{C}{B}) = (\frac{- A}{B}) (p (1) - X (1)) + (\frac{C}{B})$
88	87	eqeq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (p (2) = - (\frac{A p (1)}{B}) + (\frac{C}{B}) \leftrightarrow p (2) = (\frac{- A}{B}) (p (1) - X (1)) + (\frac{C}{B}))$
89	47 57 88	3bitr3d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (A p (1) + B p (2) = C \leftrightarrow p (2) = (\frac{- A}{B}) (p (1) - X (1)) + (\frac{C}{B}))$
90		recn	$⊢ C \in ℝ \to C \in ℂ$
91	90	adantl	$⊢ (A \in ℝ \land C \in ℝ) \to C \in ℂ$
92		recn	$⊢ A \in ℝ \to A \in ℂ$
93	92	adantr	$⊢ (A \in ℝ \land C \in ℝ) \to A \in ℂ$
94		sub32	$⊢ (C \in ℂ \land A \in ℂ \land C \in ℂ) \to C - A - C = C - C - A$
95		subid	$⊢ C \in ℂ \to C - C = 0$
96	95	3ad2ant1	$⊢ (C \in ℂ \land A \in ℂ \land C \in ℂ) \to C - C = 0$
97	96	oveq1d	$⊢ (C \in ℂ \land A \in ℂ \land C \in ℂ) \to C - C - A = 0 - A$
98		df-neg	$⊢ - A = 0 - A$
99	97 98	eqtr4di	$⊢ (C \in ℂ \land A \in ℂ \land C \in ℂ) \to C - C - A = - A$
100	94 99	eqtr2d	$⊢ (C \in ℂ \land A \in ℂ \land C \in ℂ) \to - A = C - A - C$
101	91 93 91 100	syl3anc	$⊢ (A \in ℝ \land C \in ℝ) \to - A = C - A - C$
102	101	3adant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to - A = C - A - C$
103	102	oveq1d	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{- A}{B} = \frac{C - A - C}{B}$
104	103	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{- A}{B} = \frac{C - A - C}{B}$
105	104	oveq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{- A}{B}) (p (1) - X (1)) = (\frac{C - A - C}{B}) (p (1) - X (1))$
106	105	oveq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{- A}{B}) (p (1) - X (1)) + (\frac{C}{B}) = (\frac{C - A - C}{B}) (p (1) - X (1)) + (\frac{C}{B})$
107	106	eqeq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (p (2) = (\frac{- A}{B}) (p (1) - X (1)) + (\frac{C}{B}) \leftrightarrow p (2) = (\frac{C - A - C}{B}) (p (1) - X (1)) + (\frac{C}{B}))$
108	89 107	bitrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (A p (1) + B p (2) = C \leftrightarrow p (2) = (\frac{C - A - C}{B}) (p (1) - X (1)) + (\frac{C}{B}))$
109	7	fveq1i	$⊢ Y (2) = \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (2)$
110		2ex	$⊢ 2 \in V$
111	110	a1i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to 2 \in V$
112		resubcl	$⊢ (C \in ℝ \land A \in ℝ) \to C - A \in ℝ$
113	112	ancoms	$⊢ (A \in ℝ \land C \in ℝ) \to C - A \in ℝ$
114	113	3adant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C - A \in ℝ$
115	114 35 23	redivcld	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{C - A}{B} \in ℝ$
116	76	a1i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to 1 \neq 2$
117	111 115 116	3jca	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (2 \in V \land \frac{C - A}{B} \in ℝ \land 1 \neq 2)$
118	117	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (2 \in V \land \frac{C - A}{B} \in ℝ \land 1 \neq 2)$
119		fvpr2g	$⊢ (2 \in V \land \frac{C - A}{B} \in ℝ \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (2) = \frac{C - A}{B}$
120	118 119	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (2) = \frac{C - A}{B}$
121	109 120	syl5eq	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to Y (2) = \frac{C - A}{B}$
122	6	fveq1i	$⊢ X (2) = \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2)$
123		fvpr2g	$⊢ (2 \in V \land \frac{C}{B} \in ℝ \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = \frac{C}{B}$
124	110 36 116 123	mp3an2i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (2) = \frac{C}{B}$
125	122 124	syl5eq	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X (2) = \frac{C}{B}$
126	125	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to X (2) = \frac{C}{B}$
127	121 126	oveq12d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to Y (2) - X (2) = (\frac{C - A}{B}) - (\frac{C}{B})$
128	34 8	resubcld	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C - A \in ℝ$
129	128	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C - A \in ℂ$
130		divsubdir	$⊢ (C - A \in ℂ \land C \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{C - A - C}{B} = (\frac{C - A}{B}) - (\frac{C}{B})$
131	129 50 54 130	syl3anc	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{C - A - C}{B} = (\frac{C - A}{B}) - (\frac{C}{B})$
132	131	eqcomd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (\frac{C - A}{B}) - (\frac{C}{B}) = \frac{C - A - C}{B}$
133	132	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{C - A}{B}) - (\frac{C}{B}) = \frac{C - A - C}{B}$
134	127 133	eqtr2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to \frac{C - A - C}{B} = Y (2) - X (2)$
135	134	oveq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{C - A - C}{B}) (p (1) - X (1)) = (Y (2) - X (2)) (p (1) - X (1))$
136	135	oveq1d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{C - A - C}{B}) (p (1) - X (1)) + (\frac{C}{B}) = (Y (2) - X (2)) (p (1) - X (1)) + (\frac{C}{B})$
137	136	eqeq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (p (2) = (\frac{C - A - C}{B}) (p (1) - X (1)) + (\frac{C}{B}) \leftrightarrow p (2) = (Y (2) - X (2)) (p (1) - X (1)) + (\frac{C}{B}))$
138	7	fveq1i	$⊢ Y (1) = \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (1)$
139	74 74	fvpr1	$⊢ 1 \neq 2 \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (1) = 1$
140	76 139	ax-mp	$⊢ \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (1) = 1$
141	138 140	eqtri	$⊢ Y (1) = 1$
142	74 75	fvpr1	$⊢ 1 \neq 2 \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
143	76 142	ax-mp	$⊢ \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
144	73 143	eqtri	$⊢ X (1) = 0$
145	141 144	oveq12i	$⊢ Y (1) - X (1) = 1 - 0$
146		1m0e1	$⊢ 1 - 0 = 1$
147	145 146	eqtri	$⊢ Y (1) - X (1) = 1$
148	147	a1i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to Y (1) - X (1) = 1$
149	148	oveq2d	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{Y (2) - X (2)}{Y (1) - X (1)} = \frac{Y (2) - X (2)}{1}$
150	110 115 116 119	mp3an2i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (2) = \frac{C - A}{B}$
151	109 150	syl5eq	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to Y (2) = \frac{C - A}{B}$
152	115	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{C - A}{B} \in ℂ$
153	151 152	eqeltrd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to Y (2) \in ℂ$
154	125 37	eqeltrd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X (2) \in ℂ$
155	153 154	subcld	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to Y (2) - X (2) \in ℂ$
156	155	div1d	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{Y (2) - X (2)}{1} = Y (2) - X (2)$
157	149 156	eqtrd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \frac{Y (2) - X (2)}{Y (1) - X (1)} = Y (2) - X (2)$
158	157	oveq1d	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) = (Y (2) - X (2)) (p (1) - X (1))$
159	158 125	oveq12d	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2) = (Y (2) - X (2)) (p (1) - X (1)) + (\frac{C}{B})$
160	159	adantr	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2) = (Y (2) - X (2)) (p (1) - X (1)) + (\frac{C}{B})$
161	160	eqcomd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (Y (2) - X (2)) (p (1) - X (1)) + (\frac{C}{B}) = (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2)$
162	161	eqeq2d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (p (2) = (Y (2) - X (2)) (p (1) - X (1)) + (\frac{C}{B}) \leftrightarrow p (2) = (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2))$
163	108 137 162	3bitrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land p \in P) \to (A p (1) + B p (2) = C \leftrightarrow p (2) = (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2))$
164	163	rabbidva	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| p (2) = (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2)\}$
165	5	a1i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to G = \{p \in P \| A p (1) + B p (2) = C\}$
166	74 110	pm3.2i	$⊢ (1 \in V \land 2 \in V)$
167	36 75	jctil	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (0 \in V \land \frac{C}{B} \in ℝ)$
168		fprg	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land \frac{C}{B} \in ℝ) \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} : \{1, 2\} ⟶ \{0, \frac{C}{B}\}$
169	166 167 116 168	mp3an2i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} : \{1, 2\} ⟶ \{0, \frac{C}{B}\}$
170		0red	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to 0 \in ℝ$
171	170 36	prssd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{0, \frac{C}{B}\} \subseteq ℝ$
172	169 171	fssd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} : \{1, 2\} ⟶ ℝ$
173	6	feq1i	$⊢ X : \{1, 2\} ⟶ ℝ \leftrightarrow \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} : \{1, 2\} ⟶ ℝ$
174	172 173	sylibr	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X : \{1, 2\} ⟶ ℝ$
175		reex	$⊢ ℝ \in V$
176		prex	$⊢ \{1, 2\} \in V$
177	175 176	elmap	$⊢ X \in (ℝ^{\{1, 2\}}) \leftrightarrow X : \{1, 2\} ⟶ ℝ$
178	174 177	sylibr	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X \in (ℝ^{\{1, 2\}})$
179	1	oveq2i	$⊢ ℝ^{I} = ℝ^{\{1, 2\}}$
180	3 179	eqtri	$⊢ P = ℝ^{\{1, 2\}}$
181	178 180	eleqtrrdi	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X \in P$
182	115 74	jctil	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to (1 \in V \land \frac{C - A}{B} \in ℝ)$
183		fprg	$⊢ ((1 \in V \land 2 \in V) \land (1 \in V \land \frac{C - A}{B} \in ℝ) \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} : \{1, 2\} ⟶ \{1, \frac{C - A}{B}\}$
184	166 182 116 183	mp3an2i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} : \{1, 2\} ⟶ \{1, \frac{C - A}{B}\}$
185		1red	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to 1 \in ℝ$
186	185 115	prssd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{1, \frac{C - A}{B}\} \subseteq ℝ$
187	184 186	fssd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} : \{1, 2\} ⟶ ℝ$
188	7	feq1i	$⊢ Y : \{1, 2\} ⟶ ℝ \leftrightarrow \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} : \{1, 2\} ⟶ ℝ$
189	187 188	sylibr	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to Y : \{1, 2\} ⟶ ℝ$
190	175 176	elmap	$⊢ Y \in (ℝ^{\{1, 2\}}) \leftrightarrow Y : \{1, 2\} ⟶ ℝ$
191	189 190	sylibr	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to Y \in (ℝ^{\{1, 2\}})$
192	191 180	eleqtrrdi	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to Y \in P$
193		0ne1	$⊢ 0 \neq 1$
194	77 78	ax-mp	$⊢ \{⟨1, 0⟩, ⟨2, \frac{C}{B}⟩\} (1) = 0$
195	73 194	eqtri	$⊢ X (1) = 0$
196	74 74 76	3pm3.2i	$⊢ (1 \in V \land 1 \in V \land 1 \neq 2)$
197		fvpr1g	$⊢ (1 \in V \land 1 \in V \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (1) = 1$
198	196 197	ax-mp	$⊢ \{⟨1, 1⟩, ⟨2, \frac{C - A}{B}⟩\} (1) = 1$
199	138 198	eqtri	$⊢ Y (1) = 1$
200	195 199	neeq12i	$⊢ X (1) \neq Y (1) \leftrightarrow 0 \neq 1$
201	193 200	mpbir	$⊢ X (1) \neq Y (1)$
202	201	a1i	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X (1) \neq Y (1)$
203		eqid	$⊢ \frac{Y (2) - X (2)}{Y (1) - X (1)} = \frac{Y (2) - X (2)}{Y (1) - X (1)}$
204	1 2 3 4 203	rrx2linesl	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X L Y = \{p \in P \| p (2) = (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2)\}$
205	181 192 202 204	syl3anc	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to X L Y = \{p \in P \| p (2) = (\frac{Y (2) - X (2)}{Y (1) - X (1)}) (p (1) - X (1)) + X (2)\}$
206	164 165 205	3eqtr4d	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to G = X L Y$

Metamath Proof Explorer

Theorem line2

Proof