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

Metamath Proof Explorer

Theorem line2

Proof