line2x

Description: Example for a horizontal 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\}$
	line2x.x	$⊢ X = ⟨“ 0 M ”⟩$
	line2x.y	$⊢ Y = ⟨“ 1 M ”⟩$
Assertion	line2x	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (G = X L Y \leftrightarrow (A = 0 \land M = \frac{C}{B}))$

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		line2x.x	$⊢ X = ⟨“ 0 M ”⟩$
7		line2x.y	$⊢ Y = ⟨“ 1 M ”⟩$
8	5	a1i	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to G = \{p \in P \| A p (0) + B p (1) = C\}$
9		s2len	$⊢ \|⟨“ 0 M ”⟩\| = 2$
10	9	eqcomi	$⊢ 2 = \|⟨“ 0 M ”⟩\|$
11	10	a1i	$⊢ M \in ℝ \to 2 = \|⟨“ 0 M ”⟩\|$
12		0red	$⊢ M \in ℝ \to 0 \in ℝ$
13		id	$⊢ M \in ℝ \to M \in ℝ$
14	12 13	s2cld	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ \in Word ℝ$
15	11 14	wrdfd	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ : (0 ..^2) ⟶ ℝ$
16	1	feq2i	$⊢ ⟨“ 0 M ”⟩ : I ⟶ ℝ \leftrightarrow ⟨“ 0 M ”⟩ : (0 ..^2) ⟶ ℝ$
17	15 16	sylibr	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ : I ⟶ ℝ$
18		reex	$⊢ ℝ \in V$
19	1	ovexi	$⊢ I \in V$
20	18 19	elmap	$⊢ ⟨“ 0 M ”⟩ \in (ℝ^{I}) \leftrightarrow ⟨“ 0 M ”⟩ : I ⟶ ℝ$
21	17 20	sylibr	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ \in (ℝ^{I})$
22	21 6 3	3eltr4g	$⊢ M \in ℝ \to X \in P$
23		s2len	$⊢ \|⟨“ 1 M ”⟩\| = 2$
24	23	eqcomi	$⊢ 2 = \|⟨“ 1 M ”⟩\|$
25	24	a1i	$⊢ M \in ℝ \to 2 = \|⟨“ 1 M ”⟩\|$
26		1re	$⊢ 1 \in ℝ$
27	26	a1i	$⊢ M \in ℝ \to 1 \in ℝ$
28	27 13	s2cld	$⊢ M \in ℝ \to ⟨“ 1 M ”⟩ \in Word ℝ$
29	25 28	wrdfd	$⊢ M \in ℝ \to ⟨“ 1 M ”⟩ : (0 ..^2) ⟶ ℝ$
30	1	feq2i	$⊢ ⟨“ 1 M ”⟩ : I ⟶ ℝ \leftrightarrow ⟨“ 1 M ”⟩ : (0 ..^2) ⟶ ℝ$
31	29 30	sylibr	$⊢ M \in ℝ \to ⟨“ 1 M ”⟩ : I ⟶ ℝ$
32	18 19	pm3.2i	$⊢ (ℝ \in V \land I \in V)$
33		elmapg	$⊢ (ℝ \in V \land I \in V) \to (⟨“ 1 M ”⟩ \in (ℝ^{I}) \leftrightarrow ⟨“ 1 M ”⟩ : I ⟶ ℝ)$
34	32 33	mp1i	$⊢ M \in ℝ \to (⟨“ 1 M ”⟩ \in (ℝ^{I}) \leftrightarrow ⟨“ 1 M ”⟩ : I ⟶ ℝ)$
35	31 34	mpbird	$⊢ M \in ℝ \to ⟨“ 1 M ”⟩ \in (ℝ^{I})$
36	35 7 3	3eltr4g	$⊢ M \in ℝ \to Y \in P$
37		0ne1	$⊢ 0 \neq 1$
38	37	a1i	$⊢ M \in ℝ \to 0 \neq 1$
39		0red	$⊢ (M \in ℝ \land ⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩) \to 0 \in ℝ$
40		simpl	$⊢ (M \in ℝ \land ⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩) \to M \in ℝ$
41	40 26	jctil	$⊢ (M \in ℝ \land ⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩) \to (1 \in ℝ \land M \in ℝ)$
42		simpr	$⊢ (M \in ℝ \land ⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩) \to ⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩$
43		s2eq2seq	$⊢ ((0 \in ℝ \land M \in ℝ) \land (1 \in ℝ \land M \in ℝ)) \to (⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩ \leftrightarrow (0 = 1 \land M = M))$
44	43	simprbda	$⊢ (((0 \in ℝ \land M \in ℝ) \land (1 \in ℝ \land M \in ℝ)) \land ⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩) \to 0 = 1$
45	39 40 41 42 44	syl1111anc	$⊢ (M \in ℝ \land ⟨“ 0 M ”⟩ = ⟨“ 1 M ”⟩) \to 0 = 1$
46	38 45	mteqand	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ \neq ⟨“ 1 M ”⟩$
47	46 6 7	3netr4g	$⊢ M \in ℝ \to X \neq Y$
48	22 36 47	3jca	$⊢ M \in ℝ \to (X \in P \land Y \in P \land X \neq Y)$
49	48	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (X \in P \land Y \in P \land X \neq Y)$
50		eqid	$⊢ Y (0) - X (0) = Y (0) - X (0)$
51		eqid	$⊢ Y (1) - X (1) = Y (1) - X (1)$
52		eqid	$⊢ X (1) Y (0) - X (0) Y (1) = X (1) Y (0) - X (0) Y (1)$
53	1 2 3 4 50 51 52	rrx2linest	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)\}$
54	49 53	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to X L Y = \{p \in P \| (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)\}$
55	8 54	eqeq12d	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (G = X L Y \leftrightarrow \{p \in P \| A p (0) + B p (1) = C\} = \{p \in P \| (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)\})$
56		rabbi	$⊢ \forall p \in P (A p (0) + B p (1) = C \leftrightarrow (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)) \leftrightarrow \{p \in P \| A p (0) + B p (1) = C\} = \{p \in P \| (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)\}$
57	7	fveq1i	$⊢ Y (0) = ⟨“ 1 M ”⟩ (0)$
58		s2fv0	$⊢ 1 \in ℝ \to ⟨“ 1 M ”⟩ (0) = 1$
59	26 58	mp1i	$⊢ M \in ℝ \to ⟨“ 1 M ”⟩ (0) = 1$
60	57 59	eqtrid	$⊢ M \in ℝ \to Y (0) = 1$
61	6	fveq1i	$⊢ X (0) = ⟨“ 0 M ”⟩ (0)$
62		0re	$⊢ 0 \in ℝ$
63		s2fv0	$⊢ 0 \in ℝ \to ⟨“ 0 M ”⟩ (0) = 0$
64	62 63	mp1i	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ (0) = 0$
65	61 64	eqtrid	$⊢ M \in ℝ \to X (0) = 0$
66	60 65	oveq12d	$⊢ M \in ℝ \to Y (0) - X (0) = 1 - 0$
67		1m0e1	$⊢ 1 - 0 = 1$
68	66 67	eqtrdi	$⊢ M \in ℝ \to Y (0) - X (0) = 1$
69	68	oveq1d	$⊢ M \in ℝ \to (Y (0) - X (0)) p (1) = 1 p (1)$
70	7	fveq1i	$⊢ Y (1) = ⟨“ 1 M ”⟩ (1)$
71		s2fv1	$⊢ M \in ℝ \to ⟨“ 1 M ”⟩ (1) = M$
72	70 71	eqtrid	$⊢ M \in ℝ \to Y (1) = M$
73	6	fveq1i	$⊢ X (1) = ⟨“ 0 M ”⟩ (1)$
74		s2fv1	$⊢ M \in ℝ \to ⟨“ 0 M ”⟩ (1) = M$
75	73 74	eqtrid	$⊢ M \in ℝ \to X (1) = M$
76	72 75	oveq12d	$⊢ M \in ℝ \to Y (1) - X (1) = M - M$
77		recn	$⊢ M \in ℝ \to M \in ℂ$
78	77	subidd	$⊢ M \in ℝ \to M - M = 0$
79	76 78	eqtrd	$⊢ M \in ℝ \to Y (1) - X (1) = 0$
80	79	oveq1d	$⊢ M \in ℝ \to (Y (1) - X (1)) p (0) = 0 \cdot p (0)$
81	75 60	oveq12d	$⊢ M \in ℝ \to X (1) Y (0) = M \cdot 1$
82		ax-1rid	$⊢ M \in ℝ \to M \cdot 1 = M$
83	81 82	eqtrd	$⊢ M \in ℝ \to X (1) Y (0) = M$
84	65 72	oveq12d	$⊢ M \in ℝ \to X (0) Y (1) = 0 \cdot M$
85	77	mul02d	$⊢ M \in ℝ \to 0 \cdot M = 0$
86	84 85	eqtrd	$⊢ M \in ℝ \to X (0) Y (1) = 0$
87	83 86	oveq12d	$⊢ M \in ℝ \to X (1) Y (0) - X (0) Y (1) = M - 0$
88	77	subid1d	$⊢ M \in ℝ \to M - 0 = M$
89	87 88	eqtrd	$⊢ M \in ℝ \to X (1) Y (0) - X (0) Y (1) = M$
90	80 89	oveq12d	$⊢ M \in ℝ \to (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1) = 0 \cdot p (0) + M$
91	69 90	eqeq12d	$⊢ M \in ℝ \to ((Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1) \leftrightarrow 1 p (1) = 0 \cdot p (0) + M)$
92	91	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to ((Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1) \leftrightarrow 1 p (1) = 0 \cdot p (0) + M)$
93	1 3	rrx2pyel	$⊢ p \in P \to p (1) \in ℝ$
94	93	recnd	$⊢ p \in P \to p (1) \in ℂ$
95	94	mullidd	$⊢ p \in P \to 1 p (1) = p (1)$
96	1 3	rrx2pxel	$⊢ p \in P \to p (0) \in ℝ$
97	96	recnd	$⊢ p \in P \to p (0) \in ℂ$
98	97	mul02d	$⊢ p \in P \to 0 \cdot p (0) = 0$
99	98	oveq1d	$⊢ p \in P \to 0 \cdot p (0) + M = 0 + M$
100	95 99	eqeq12d	$⊢ p \in P \to (1 p (1) = 0 \cdot p (0) + M \leftrightarrow p (1) = 0 + M)$
101	92 100	sylan9bb	$⊢ (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land p \in P) \to ((Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1) \leftrightarrow p (1) = 0 + M)$
102	101	bibi2d	$⊢ (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land p \in P) \to ((A p (0) + B p (1) = C \leftrightarrow (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)) \leftrightarrow (A p (0) + B p (1) = C \leftrightarrow p (1) = 0 + M))$
103	102	ralbidva	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)) \leftrightarrow \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = 0 + M))$
104	77	addlidd	$⊢ M \in ℝ \to 0 + M = M$
105	104	adantr	$⊢ (M \in ℝ \land p \in P) \to 0 + M = M$
106	105	eqeq2d	$⊢ (M \in ℝ \land p \in P) \to (p (1) = 0 + M \leftrightarrow p (1) = M)$
107	106	bibi2d	$⊢ (M \in ℝ \land p \in P) \to ((A p (0) + B p (1) = C \leftrightarrow p (1) = 0 + M) \leftrightarrow (A p (0) + B p (1) = C \leftrightarrow p (1) = M))$
108	107	ralbidva	$⊢ M \in ℝ \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = 0 + M) \leftrightarrow \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = M))$
109	108	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = 0 + M) \leftrightarrow \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = M))$
110	1 2 3 4 5 6 7	line2xlem	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = M) \to (A = 0 \land M = \frac{C}{B}))$
111		oveq1	$⊢ A = 0 \to A p (0) = 0 \cdot p (0)$
112	111	adantr	$⊢ (A = 0 \land M = \frac{C}{B}) \to A p (0) = 0 \cdot p (0)$
113	112	ad2antlr	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to A p (0) = 0 \cdot p (0)$
114	98	adantl	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to 0 \cdot p (0) = 0$
115	113 114	eqtrd	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to A p (0) = 0$
116	115	oveq1d	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to A p (0) + B p (1) = 0 + B p (1)$
117		recn	$⊢ B \in ℝ \to B \in ℂ$
118	117	adantr	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℂ$
119	118	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \in ℂ$
120	119	ad3antrrr	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to B \in ℂ$
121	94	adantl	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to p (1) \in ℂ$
122	120 121	mulcld	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to B p (1) \in ℂ$
123	122	addlidd	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to 0 + B p (1) = B p (1)$
124	116 123	eqtrd	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to A p (0) + B p (1) = B p (1)$
125	124	eqeq1d	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to (A p (0) + B p (1) = C \leftrightarrow B p (1) = C)$
126		simp3	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℝ$
127	126	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℂ$
128	127	ad3antrrr	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to C \in ℂ$
129		simp2r	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \neq 0$
130	129	ad3antrrr	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to B \neq 0$
131	128 120 121 130	divmuld	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to (\frac{C}{B} = p (1) \leftrightarrow B p (1) = C)$
132		simpr	$⊢ (A = 0 \land M = \frac{C}{B}) \to M = \frac{C}{B}$
133	132	eqcomd	$⊢ (A = 0 \land M = \frac{C}{B}) \to \frac{C}{B} = M$
134	133	ad2antlr	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to \frac{C}{B} = M$
135	134	eqeq1d	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to (\frac{C}{B} = p (1) \leftrightarrow M = p (1))$
136	125 131 135	3bitr2d	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to (A p (0) + B p (1) = C \leftrightarrow M = p (1))$
137		eqcom	$⊢ M = p (1) \leftrightarrow p (1) = M$
138	136 137	bitrdi	$⊢ ((((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \land p \in P) \to (A p (0) + B p (1) = C \leftrightarrow p (1) = M)$
139	138	ralrimiva	$⊢ (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land (A = 0 \land M = \frac{C}{B})) \to \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = M)$
140	139	ex	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to ((A = 0 \land M = \frac{C}{B}) \to \forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = M))$
141	110 140	impbid	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow p (1) = M) \leftrightarrow (A = 0 \land M = \frac{C}{B}))$
142	103 109 141	3bitrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (0) + B p (1) = C \leftrightarrow (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)) \leftrightarrow (A = 0 \land M = \frac{C}{B}))$
143	56 142	bitr3id	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\{p \in P \| A p (0) + B p (1) = C\} = \{p \in P \| (Y (0) - X (0)) p (1) = (Y (1) - X (1)) p (0) + X (1) Y (0) - X (0) Y (1)\} \leftrightarrow (A = 0 \land M = \frac{C}{B}))$
144	55 143	bitrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (G = X L Y \leftrightarrow (A = 0 \land M = \frac{C}{B}))$

Metamath Proof Explorer

Theorem line2x

Proof