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 = \{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\}$
	line2x.x	$⊢ X = \{⟨1, 0⟩, ⟨2, M⟩\}$
	line2x.y	$⊢ Y = \{⟨1, 1⟩, ⟨2, 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 = \{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		line2x.x	$⊢ X = \{⟨1, 0⟩, ⟨2, M⟩\}$
7		line2x.y	$⊢ Y = \{⟨1, 1⟩, ⟨2, 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 (1) + B p (2) = C\}$
9		1ex	$⊢ 1 \in V$
10		2ex	$⊢ 2 \in V$
11	9 10	pm3.2i	$⊢ (1 \in V \land 2 \in V)$
12		c0ex	$⊢ 0 \in V$
13	12	jctl	$⊢ M \in ℝ \to (0 \in V \land M \in ℝ)$
14		1ne2	$⊢ 1 \neq 2$
15	14	a1i	$⊢ M \in ℝ \to 1 \neq 2$
16		fprg	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ \{0, M\}$
17		0red	$⊢ (1 \in V \land 2 \in V) \to 0 \in ℝ$
18		simpr	$⊢ (0 \in V \land M \in ℝ) \to M \in ℝ$
19	17 18	anim12i	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ)) \to (0 \in ℝ \land M \in ℝ)$
20	19	3adant3	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to (0 \in ℝ \land M \in ℝ)$
21		prssi	$⊢ (0 \in ℝ \land M \in ℝ) \to \{0, M\} \subseteq ℝ$
22	20 21	syl	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to \{0, M\} \subseteq ℝ$
23	16 22	fssd	$⊢ ((1 \in V \land 2 \in V) \land (0 \in V \land M \in ℝ) \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
24	11 13 15 23	mp3an2i	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
25	1	feq2i	$⊢ \{⟨1, 0⟩, ⟨2, M⟩\} : I ⟶ ℝ \leftrightarrow \{⟨1, 0⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
26	24 25	sylibr	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} : I ⟶ ℝ$
27		reex	$⊢ ℝ \in V$
28		prex	$⊢ \{1, 2\} \in V$
29	1 28	eqeltri	$⊢ I \in V$
30	27 29	elmap	$⊢ \{⟨1, 0⟩, ⟨2, M⟩\} \in (ℝ^{I}) \leftrightarrow \{⟨1, 0⟩, ⟨2, M⟩\} : I ⟶ ℝ$
31	26 30	sylibr	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} \in (ℝ^{I})$
32	31 6 3	3eltr4g	$⊢ M \in ℝ \to X \in P$
33	9	jctl	$⊢ M \in ℝ \to (1 \in V \land M \in ℝ)$
34		fprg	$⊢ ((1 \in V \land 2 \in V) \land (1 \in V \land M \in ℝ) \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ \{1, M\}$
35	11 33 15 34	mp3an2i	$⊢ M \in ℝ \to \{⟨1, 1⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ \{1, M\}$
36		1re	$⊢ 1 \in ℝ$
37		prssi	$⊢ (1 \in ℝ \land M \in ℝ) \to \{1, M\} \subseteq ℝ$
38	36 37	mpan	$⊢ M \in ℝ \to \{1, M\} \subseteq ℝ$
39	35 38	fssd	$⊢ M \in ℝ \to \{⟨1, 1⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
40	1	feq2i	$⊢ \{⟨1, 1⟩, ⟨2, M⟩\} : I ⟶ ℝ \leftrightarrow \{⟨1, 1⟩, ⟨2, M⟩\} : \{1, 2\} ⟶ ℝ$
41	39 40	sylibr	$⊢ M \in ℝ \to \{⟨1, 1⟩, ⟨2, M⟩\} : I ⟶ ℝ$
42	27 29	pm3.2i	$⊢ (ℝ \in V \land I \in V)$
43		elmapg	$⊢ (ℝ \in V \land I \in V) \to (\{⟨1, 1⟩, ⟨2, M⟩\} \in (ℝ^{I}) \leftrightarrow \{⟨1, 1⟩, ⟨2, M⟩\} : I ⟶ ℝ)$
44	42 43	mp1i	$⊢ M \in ℝ \to (\{⟨1, 1⟩, ⟨2, M⟩\} \in (ℝ^{I}) \leftrightarrow \{⟨1, 1⟩, ⟨2, M⟩\} : I ⟶ ℝ)$
45	41 44	mpbird	$⊢ M \in ℝ \to \{⟨1, 1⟩, ⟨2, M⟩\} \in (ℝ^{I})$
46	45 7 3	3eltr4g	$⊢ M \in ℝ \to Y \in P$
47		opex	$⊢ ⟨1, 0⟩ \in V$
48		opex	$⊢ ⟨2, M⟩ \in V$
49	47 48	pm3.2i	$⊢ (⟨1, 0⟩ \in V \land ⟨2, M⟩ \in V)$
50		opex	$⊢ ⟨1, 1⟩ \in V$
51	50 48	pm3.2i	$⊢ (⟨1, 1⟩ \in V \land ⟨2, M⟩ \in V)$
52	49 51	pm3.2i	$⊢ ((⟨1, 0⟩ \in V \land ⟨2, M⟩ \in V) \land (⟨1, 1⟩ \in V \land ⟨2, M⟩ \in V))$
53	14	orci	$⊢ (1 \neq 2 \lor 0 \neq M)$
54	9 12	opthne	$⊢ ⟨1, 0⟩ \neq ⟨2, M⟩ \leftrightarrow (1 \neq 2 \lor 0 \neq M)$
55	53 54	mpbir	$⊢ ⟨1, 0⟩ \neq ⟨2, M⟩$
56	55	a1i	$⊢ M \in ℝ \to ⟨1, 0⟩ \neq ⟨2, M⟩$
57		0ne1	$⊢ 0 \neq 1$
58	57	olci	$⊢ (1 \neq 1 \lor 0 \neq 1)$
59	9 12	opthne	$⊢ ⟨1, 0⟩ \neq ⟨1, 1⟩ \leftrightarrow (1 \neq 1 \lor 0 \neq 1)$
60	58 59	mpbir	$⊢ ⟨1, 0⟩ \neq ⟨1, 1⟩$
61	56 60	jctil	$⊢ M \in ℝ \to (⟨1, 0⟩ \neq ⟨1, 1⟩ \land ⟨1, 0⟩ \neq ⟨2, M⟩)$
62	61	orcd	$⊢ M \in ℝ \to ((⟨1, 0⟩ \neq ⟨1, 1⟩ \land ⟨1, 0⟩ \neq ⟨2, M⟩) \lor (⟨2, M⟩ \neq ⟨1, 1⟩ \land ⟨2, M⟩ \neq ⟨2, M⟩))$
63		prneimg	$⊢ ((⟨1, 0⟩ \in V \land ⟨2, M⟩ \in V) \land (⟨1, 1⟩ \in V \land ⟨2, M⟩ \in V)) \to (((⟨1, 0⟩ \neq ⟨1, 1⟩ \land ⟨1, 0⟩ \neq ⟨2, M⟩) \lor (⟨2, M⟩ \neq ⟨1, 1⟩ \land ⟨2, M⟩ \neq ⟨2, M⟩)) \to \{⟨1, 0⟩, ⟨2, M⟩\} \neq \{⟨1, 1⟩, ⟨2, M⟩\})$
64	52 62 63	mpsyl	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} \neq \{⟨1, 1⟩, ⟨2, M⟩\}$
65	64 6 7	3netr4g	$⊢ M \in ℝ \to X \neq Y$
66	32 46 65	3jca	$⊢ M \in ℝ \to (X \in P \land Y \in P \land X \neq Y)$
67	66	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)$
68		eqid	$⊢ Y (1) - X (1) = Y (1) - X (1)$
69		eqid	$⊢ Y (2) - X (2) = Y (2) - X (2)$
70		eqid	$⊢ X (2) Y (1) - X (1) Y (2) = X (2) Y (1) - X (1) Y (2)$
71	1 2 3 4 68 69 70	rrx2linest	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)\}$
72	67 71	syl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to X L Y = \{p \in P \| (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)\}$
73	8 72	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 (1) + B p (2) = C\} = \{p \in P \| (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)\})$
74		rabbi	$⊢ \forall p \in P (A p (1) + B p (2) = C \leftrightarrow (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)) \leftrightarrow \{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)\}$
75	7	fveq1i	$⊢ Y (1) = \{⟨1, 1⟩, ⟨2, M⟩\} (1)$
76	9 9 14	3pm3.2i	$⊢ (1 \in V \land 1 \in V \land 1 \neq 2)$
77		fvpr1g	$⊢ (1 \in V \land 1 \in V \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, M⟩\} (1) = 1$
78	76 77	mp1i	$⊢ M \in ℝ \to \{⟨1, 1⟩, ⟨2, M⟩\} (1) = 1$
79	75 78	syl5eq	$⊢ M \in ℝ \to Y (1) = 1$
80	6	fveq1i	$⊢ X (1) = \{⟨1, 0⟩, ⟨2, M⟩\} (1)$
81	9 12 14	3pm3.2i	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2)$
82		fvpr1g	$⊢ (1 \in V \land 0 \in V \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} (1) = 0$
83	81 82	mp1i	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} (1) = 0$
84	80 83	syl5eq	$⊢ M \in ℝ \to X (1) = 0$
85	79 84	oveq12d	$⊢ M \in ℝ \to Y (1) - X (1) = 1 - 0$
86		1m0e1	$⊢ 1 - 0 = 1$
87	85 86	eqtrdi	$⊢ M \in ℝ \to Y (1) - X (1) = 1$
88	87	oveq1d	$⊢ M \in ℝ \to (Y (1) - X (1)) p (2) = 1 p (2)$
89	7	fveq1i	$⊢ Y (2) = \{⟨1, 1⟩, ⟨2, M⟩\} (2)$
90		fvpr2g	$⊢ (2 \in V \land M \in ℝ \land 1 \neq 2) \to \{⟨1, 1⟩, ⟨2, M⟩\} (2) = M$
91	10 14 90	mp3an13	$⊢ M \in ℝ \to \{⟨1, 1⟩, ⟨2, M⟩\} (2) = M$
92	89 91	syl5eq	$⊢ M \in ℝ \to Y (2) = M$
93	6	fveq1i	$⊢ X (2) = \{⟨1, 0⟩, ⟨2, M⟩\} (2)$
94		fvpr2g	$⊢ (2 \in V \land M \in ℝ \land 1 \neq 2) \to \{⟨1, 0⟩, ⟨2, M⟩\} (2) = M$
95	10 14 94	mp3an13	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} (2) = M$
96	93 95	syl5eq	$⊢ M \in ℝ \to X (2) = M$
97	92 96	oveq12d	$⊢ M \in ℝ \to Y (2) - X (2) = M - M$
98		recn	$⊢ M \in ℝ \to M \in ℂ$
99	98	subidd	$⊢ M \in ℝ \to M - M = 0$
100	97 99	eqtrd	$⊢ M \in ℝ \to Y (2) - X (2) = 0$
101	100	oveq1d	$⊢ M \in ℝ \to (Y (2) - X (2)) p (1) = 0 \cdot p (1)$
102	9 9 15 77	mp3an12i	$⊢ M \in ℝ \to \{⟨1, 1⟩, ⟨2, M⟩\} (1) = 1$
103	75 102	syl5eq	$⊢ M \in ℝ \to Y (1) = 1$
104	96 103	oveq12d	$⊢ M \in ℝ \to X (2) Y (1) = M \cdot 1$
105		ax-1rid	$⊢ M \in ℝ \to M \cdot 1 = M$
106	104 105	eqtrd	$⊢ M \in ℝ \to X (2) Y (1) = M$
107	9 12 15 82	mp3an12i	$⊢ M \in ℝ \to \{⟨1, 0⟩, ⟨2, M⟩\} (1) = 0$
108	80 107	syl5eq	$⊢ M \in ℝ \to X (1) = 0$
109	108 92	oveq12d	$⊢ M \in ℝ \to X (1) Y (2) = 0 \cdot M$
110	98	mul02d	$⊢ M \in ℝ \to 0 \cdot M = 0$
111	109 110	eqtrd	$⊢ M \in ℝ \to X (1) Y (2) = 0$
112	106 111	oveq12d	$⊢ M \in ℝ \to X (2) Y (1) - X (1) Y (2) = M - 0$
113	98	subid1d	$⊢ M \in ℝ \to M - 0 = M$
114	112 113	eqtrd	$⊢ M \in ℝ \to X (2) Y (1) - X (1) Y (2) = M$
115	101 114	oveq12d	$⊢ M \in ℝ \to (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2) = 0 \cdot p (1) + M$
116	88 115	eqeq12d	$⊢ M \in ℝ \to ((Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2) \leftrightarrow 1 p (2) = 0 \cdot p (1) + M)$
117	116	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to ((Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2) \leftrightarrow 1 p (2) = 0 \cdot p (1) + M)$
118	1 3	rrx2pyel	$⊢ p \in P \to p (2) \in ℝ$
119	118	recnd	$⊢ p \in P \to p (2) \in ℂ$
120	119	mulid2d	$⊢ p \in P \to 1 p (2) = p (2)$
121	1 3	rrx2pxel	$⊢ p \in P \to p (1) \in ℝ$
122	121	recnd	$⊢ p \in P \to p (1) \in ℂ$
123	122	mul02d	$⊢ p \in P \to 0 \cdot p (1) = 0$
124	123	oveq1d	$⊢ p \in P \to 0 \cdot p (1) + M = 0 + M$
125	120 124	eqeq12d	$⊢ p \in P \to (1 p (2) = 0 \cdot p (1) + M \leftrightarrow p (2) = 0 + M)$
126	117 125	sylan9bb	$⊢ (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land p \in P) \to ((Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2) \leftrightarrow p (2) = 0 + M)$
127	126	bibi2d	$⊢ (((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \land p \in P) \to ((A p (1) + B p (2) = C \leftrightarrow (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)) \leftrightarrow (A p (1) + B p (2) = C \leftrightarrow p (2) = 0 + M))$
128	127	ralbidva	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)) \leftrightarrow \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = 0 + M))$
129	98	addid2d	$⊢ M \in ℝ \to 0 + M = M$
130	129	adantr	$⊢ (M \in ℝ \land p \in P) \to 0 + M = M$
131	130	eqeq2d	$⊢ (M \in ℝ \land p \in P) \to (p (2) = 0 + M \leftrightarrow p (2) = M)$
132	131	bibi2d	$⊢ (M \in ℝ \land p \in P) \to ((A p (1) + B p (2) = C \leftrightarrow p (2) = 0 + M) \leftrightarrow (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
133	132	ralbidva	$⊢ M \in ℝ \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = 0 + M) \leftrightarrow \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
134	133	adantl	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = 0 + M) \leftrightarrow \forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M))$
135	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 (1) + B p (2) = C \leftrightarrow p (2) = M) \to (A = 0 \land M = \frac{C}{B}))$
136		oveq1	$⊢ A = 0 \to A p (1) = 0 \cdot p (1)$
137	136	adantr	$⊢ (A = 0 \land M = \frac{C}{B}) \to A p (1) = 0 \cdot p (1)$
138	137	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 (1) = 0 \cdot p (1)$
139	123	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 (1) = 0$
140	138 139	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 (1) = 0$
141	140	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 (1) + B p (2) = 0 + B p (2)$
142		recn	$⊢ B \in ℝ \to B \in ℂ$
143	142	adantr	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℂ$
144	143	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \in ℂ$
145	144	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 ℂ$
146	119	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 (2) \in ℂ$
147	145 146	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 (2) \in ℂ$
148	147	addid2d	$⊢ ((((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 (2) = B p (2)$
149	141 148	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 (1) + B p (2) = B p (2)$
150	149	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 (1) + B p (2) = C \leftrightarrow B p (2) = C)$
151		simp3	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℝ$
152	151	recnd	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to C \in ℂ$
153	152	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 ℂ$
154		simpl	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℝ$
155	154	recnd	$⊢ (B \in ℝ \land B \neq 0) \to B \in ℂ$
156	155	3ad2ant2	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \in ℂ$
157	156	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 ℂ$
158		simp2r	$⊢ (A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \to B \neq 0$
159	158	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$
160	153 157 146 159	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 (2) \leftrightarrow B p (2) = C)$
161		simpr	$⊢ (A = 0 \land M = \frac{C}{B}) \to M = \frac{C}{B}$
162	161	eqcomd	$⊢ (A = 0 \land M = \frac{C}{B}) \to \frac{C}{B} = M$
163	162	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$
164	163	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 (2) \leftrightarrow M = p (2))$
165	150 160 164	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 (1) + B p (2) = C \leftrightarrow M = p (2))$
166		eqcom	$⊢ M = p (2) \leftrightarrow p (2) = M$
167	165 166	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 (1) + B p (2) = C \leftrightarrow p (2) = M)$
168	167	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 (1) + B p (2) = C \leftrightarrow p (2) = M)$
169	168	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 (1) + B p (2) = C \leftrightarrow p (2) = M))$
170	135 169	impbid	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow p (2) = M) \leftrightarrow (A = 0 \land M = \frac{C}{B}))$
171	128 134 170	3bitrd	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\forall p \in P (A p (1) + B p (2) = C \leftrightarrow (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)) \leftrightarrow (A = 0 \land M = \frac{C}{B}))$
172	74 171	bitr3id	$⊢ ((A \in ℝ \land (B \in ℝ \land B \neq 0) \land C \in ℝ) \land M \in ℝ) \to (\{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| (Y (1) - X (1)) p (2) = (Y (2) - X (2)) p (1) + X (2) Y (1) - X (1) Y (2)\} \leftrightarrow (A = 0 \land M = \frac{C}{B}))$
173	73 172	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