line2x - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > line2x		Structured version Visualization version GIF version

Theorem line2x 45168

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

**Hypotheses**
Ref	Expression
line2.i	⊢ 𝐼 = {1, 2}
line2.e	⊢ 𝐸 = (ℝ^‘𝐼)
line2.p	⊢ 𝑃 = (ℝ ↑_m 𝐼)
line2.l	⊢ 𝐿 = (Line_M‘𝐸)
line2.g	⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}
line2x.x	⊢ 𝑋 = {⟨1, 0⟩, ⟨2, 𝑀⟩}
line2x.y	⊢ 𝑌 = {⟨1, 1⟩, ⟨2, 𝑀⟩}

**Assertion**
Ref	Expression
line2x	⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))

Distinct variable groups: 𝐴,𝑝 𝐵,𝑝 𝐶,𝑝 𝐸,𝑝 𝐼,𝑝 𝑃,𝑝 𝑋,𝑝 𝑌,𝑝 𝑀,𝑝 Allowed substitution hints: 𝐺(𝑝) 𝐿(𝑝)

**Proof of Theorem line2x**
Step	Hyp	Ref	Expression
1		line2.g	. . . 4 ⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}
2	1	a1i 11	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶})
3		1ex 10626	. . . . . . . . . . 11 ⊢ 1 ∈ V
4		2ex 11702	. . . . . . . . . . 11 ⊢ 2 ∈ V
5	3, 4	pm3.2i 474	. . . . . . . . . 10 ⊢ (1 ∈ V ∧ 2 ∈ V)
6		c0ex 10624	. . . . . . . . . . 11 ⊢ 0 ∈ V
7	6	jctl 527	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (0 ∈ V ∧ 𝑀 ∈ ℝ))
8		1ne2 11833	. . . . . . . . . . 11 ⊢ 1 ≠ 2
9	8	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → 1 ≠ 2)
10		fprg 6894	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{0, 𝑀})
11		0red 10633	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ V ∧ 2 ∈ V) → 0 ∈ ℝ)
12		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ V ∧ 𝑀 ∈ ℝ) → 𝑀 ∈ ℝ)
13	11, 12	anim12i 615	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ)) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
14	13	3adant3 1129	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
15		prssi 4714	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {0, 𝑀} ⊆ ℝ)
16	14, 15	syl 17	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0, 𝑀} ⊆ ℝ)
17	10, 16	fssd 6502	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
18	5, 7, 9, 17	mp3an2i 1463	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
19		line2.i	. . . . . . . . . 10 ⊢ 𝐼 = {1, 2}
20	19	feq2i 6479	. . . . . . . . 9 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
21	18, 20	sylibr 237	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
22		reex 10617	. . . . . . . . 9 ⊢ ℝ ∈ V
23		prex 5298	. . . . . . . . . 10 ⊢ {1, 2} ∈ V
24	19, 23	eqeltri 2886	. . . . . . . . 9 ⊢ 𝐼 ∈ V
25	22, 24	elmap 8418	. . . . . . . 8 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
26	21, 25	sylibr 237	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼))
27		line2x.x	. . . . . . 7 ⊢ 𝑋 = {⟨1, 0⟩, ⟨2, 𝑀⟩}
28		line2.p	. . . . . . 7 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
29	26, 27, 28	3eltr4g 2907	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃)
30	3	jctl 527	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (1 ∈ V ∧ 𝑀 ∈ ℝ))
31		fprg 6894	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
32	5, 30, 9, 31	mp3an2i 1463	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
33		1re 10630	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
34		prssi 4714	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {1, 𝑀} ⊆ ℝ)
35	33, 34	mpan 689	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {1, 𝑀} ⊆ ℝ)
36	32, 35	fssd 6502	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
37	19	feq2i 6479	. . . . . . . . 9 ⊢ ({⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
38	36, 37	sylibr 237	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
39	22, 24	pm3.2i 474	. . . . . . . . 9 ⊢ (ℝ ∈ V ∧ 𝐼 ∈ V)
40		elmapg 8402	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ 𝐼 ∈ V) → ({⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ))
41	39, 40	mp1i 13	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ))
42	38, 41	mpbird 260	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼))
43		line2x.y	. . . . . . 7 ⊢ 𝑌 = {⟨1, 1⟩, ⟨2, 𝑀⟩}
44	42, 43, 28	3eltr4g 2907	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑌 ∈ 𝑃)
45		opex 5321	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ∈ V
46		opex 5321	. . . . . . . . . 10 ⊢ ⟨2, 𝑀⟩ ∈ V
47	45, 46	pm3.2i 474	. . . . . . . . 9 ⊢ (⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
48		opex 5321	. . . . . . . . . 10 ⊢ ⟨1, 1⟩ ∈ V
49	48, 46	pm3.2i 474	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
50	47, 49	pm3.2i 474	. . . . . . . 8 ⊢ ((⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V) ∧ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V))
51	8	orci 862	. . . . . . . . . . . 12 ⊢ (1 ≠ 2 ∨ 0 ≠ 𝑀)
52	3, 6	opthne 5339	. . . . . . . . . . . 12 ⊢ (⟨1, 0⟩ ≠ ⟨2, 𝑀⟩ ↔ (1 ≠ 2 ∨ 0 ≠ 𝑀))
53	51, 52	mpbir 234	. . . . . . . . . . 11 ⊢ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩
54	53	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩)
55		0ne1 11696	. . . . . . . . . . . 12 ⊢ 0 ≠ 1
56	55	olci 863	. . . . . . . . . . 11 ⊢ (1 ≠ 1 ∨ 0 ≠ 1)
57	3, 6	opthne 5339	. . . . . . . . . . 11 ⊢ (⟨1, 0⟩ ≠ ⟨1, 1⟩ ↔ (1 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 234	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ≠ ⟨1, 1⟩
59	54, 58	jctil 523	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩))
60	59	orcd 870	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩) ∨ (⟨2, 𝑀⟩ ≠ ⟨1, 1⟩ ∧ ⟨2, 𝑀⟩ ≠ ⟨2, 𝑀⟩)))
61		prneimg 4745	. . . . . . . 8 ⊢ (((⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V) ∧ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)) → (((⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩) ∨ (⟨2, 𝑀⟩ ≠ ⟨1, 1⟩ ∧ ⟨2, 𝑀⟩ ≠ ⟨2, 𝑀⟩)) → {⟨1, 0⟩, ⟨2, 𝑀⟩} ≠ {⟨1, 1⟩, ⟨2, 𝑀⟩}))
62	50, 60, 61	mpsyl 68	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩} ≠ {⟨1, 1⟩, ⟨2, 𝑀⟩})
63	62, 27, 43	3netr4g 3066	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ≠ 𝑌)
64	29, 44, 63	3jca 1125	. . . . 5 ⊢ (𝑀 ∈ ℝ → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
65	64	adantl 485	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
66		line2.e	. . . . 5 ⊢ 𝐸 = (ℝ^‘𝐼)
67		line2.l	. . . . 5 ⊢ 𝐿 = (Line_M‘𝐸)
68		eqid 2798	. . . . 5 ⊢ ((𝑌‘1) − (𝑋‘1)) = ((𝑌‘1) − (𝑋‘1))
69		eqid 2798	. . . . 5 ⊢ ((𝑌‘2) − (𝑋‘2)) = ((𝑌‘2) − (𝑋‘2))
70		eqid 2798	. . . . 5 ⊢ (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))
71	19, 66, 28, 67, 68, 69, 70	rrx2linest 45156	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))})
72	65, 71	syl 17	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))})
73	2, 72	eqeq12d 2814	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))}))
74		rabbi 3336	. . 3 ⊢ (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))})
75	43	fveq1i 6646	. . . . . . . . . . . . 13 ⊢ (𝑌‘1) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1)
76	3, 3, 8	3pm3.2i 1336	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2)
77		fvpr1g 6931	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
78	76, 77	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
79	75, 78	syl5eq 2845	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
80	27	fveq1i 6646	. . . . . . . . . . . . 13 ⊢ (𝑋‘1) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1)
81	3, 6, 8	3pm3.2i 1336	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2)
82		fvpr1g 6931	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
83	81, 82	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
84	80, 83	syl5eq 2845	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
85	79, 84	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = (1 − 0))
86		1m0e1 11746	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
87	85, 86	eqtrdi 2849	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = 1)
88	87	oveq1d 7150	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = (1 · (𝑝‘2)))
89	43	fveq1i 6646	. . . . . . . . . . . . . 14 ⊢ (𝑌‘2) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2)
90		fvpr2g 6932	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
91	4, 8, 90	mp3an13 1449	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
92	89, 91	syl5eq 2845	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑌‘2) = 𝑀)
93	27	fveq1i 6646	. . . . . . . . . . . . . 14 ⊢ (𝑋‘2) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2)
94		fvpr2g 6932	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
95	4, 8, 94	mp3an13 1449	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
96	93, 95	syl5eq 2845	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑋‘2) = 𝑀)
97	92, 96	oveq12d 7153	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = (𝑀 − 𝑀))
98		recn 10616	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → 𝑀 ∈ ℂ)
99	98	subidd 10974	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑀 − 𝑀) = 0)
100	97, 99	eqtrd 2833	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = 0)
101	100	oveq1d 7150	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = (0 · (𝑝‘1)))
102	3, 3, 9, 77	mp3an12i 1462	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
103	75, 102	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
104	96, 103	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = (𝑀 · 1))
105		ax-1rid 10596	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑀 · 1) = 𝑀)
106	104, 105	eqtrd 2833	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = 𝑀)
107	3, 6, 9, 82	mp3an12i 1462	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
108	80, 107	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
109	108, 92	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = (0 · 𝑀))
110	98	mul02d 10827	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (0 · 𝑀) = 0)
111	109, 110	eqtrd 2833	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = 0)
112	106, 111	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (𝑀 − 0))
113	98	subid1d 10975	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 0) = 𝑀)
114	112, 113	eqtrd 2833	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = 𝑀)
115	101, 114	oveq12d 7153	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) = ((0 · (𝑝‘1)) + 𝑀))
116	88, 115	eqeq12d 2814	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
117	116	adantl 485	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
118	19, 28	rrx2pyel 45126	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ)
119	118	recnd 10658	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ)
120	119	mulid2d 10648	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → (1 · (𝑝‘2)) = (𝑝‘2))
121	19, 28	rrx2pxel 45125	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
122	121	recnd 10658	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
123	122	mul02d 10827	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘1)) = 0)
124	123	oveq1d 7150	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → ((0 · (𝑝‘1)) + 𝑀) = (0 + 𝑀))
125	120, 124	eqeq12d 2814	. . . . . . 7 ⊢ (𝑝 ∈ 𝑃 → ((1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀) ↔ (𝑝‘2) = (0 + 𝑀)))
126	117, 125	sylan9bb 513	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (𝑝‘2) = (0 + 𝑀)))
127	126	bibi2d 346	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
128	127	ralbidva 3161	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
129	98	addid2d 10830	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (0 + 𝑀) = 𝑀)
130	129	adantr 484	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → (0 + 𝑀) = 𝑀)
131	130	eqeq2d 2809	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (0 + 𝑀) ↔ (𝑝‘2) = 𝑀))
132	131	bibi2d 346	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
133	132	ralbidva 3161	. . . . 5 ⊢ (𝑀 ∈ ℝ → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
134	133	adantl 485	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
135	19, 66, 28, 67, 1, 27, 43	line2xlem 45167	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) → (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
136		oveq1 7142	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
137	136	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
138	137	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
139	123	adantl 485	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 · (𝑝‘1)) = 0)
140	138, 139	eqtrd 2833	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = 0)
141	140	oveq1d 7150	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (0 + (𝐵 · (𝑝‘2))))
142		recn 10616	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
143	142	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
144	143	3ad2ant2 1131	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
145	144	ad3antrrr 729	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
146	119	adantl 485	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℂ)
147	145, 146	mulcld 10650	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ)
148	147	addid2d 10830	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
149	141, 148	eqtrd 2833	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
150	149	eqeq1d 2800	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝐵 · (𝑝‘2)) = 𝐶))
151		simp3 1135	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
152	151	recnd 10658	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
153	152	ad3antrrr 729	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ)
154		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℝ)
155	154	recnd 10658	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
156	155	3ad2ant2 1131	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
157	156	ad3antrrr 729	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
158		simp2r 1197	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ≠ 0)
159	158	ad3antrrr 729	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ≠ 0)
160	153, 157, 146, 159	divmuld 11427	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ (𝐵 · (𝑝‘2)) = 𝐶))
161		simpr 488	. . . . . . . . . . . 12 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → 𝑀 = (𝐶 / 𝐵))
162	161	eqcomd 2804	. . . . . . . . . . 11 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐶 / 𝐵) = 𝑀)
163	162	ad2antlr 726	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) = 𝑀)
164	163	eqeq1d 2800	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ 𝑀 = (𝑝‘2)))
165	150, 160, 164	3bitr2d 310	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ 𝑀 = (𝑝‘2)))
166		eqcom 2805	. . . . . . . 8 ⊢ (𝑀 = (𝑝‘2) ↔ (𝑝‘2) = 𝑀)
167	165, 166	syl6bb 290	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
168	167	ralrimiva 3149	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
169	168	ex 416	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
170	135, 169	impbid 215	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
171	128, 134, 170	3bitrd 308	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
172	74, 171	bitr3id 288	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))} ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
173	73, 172	bitrd 282	1 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 {crab 3110 Vcvv 3441 ⊆ wss 3881 {cpr 4527 ⟨cop 4531 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ↑_m cmap 8389 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 · cmul 10531 − cmin 10859 / cdiv 11286 2c2 11680 ℝ^crrx 23987 Line_Mcline 45141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604 ax-addf 10605 ax-mulf 10606

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-tpos 7875 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-er 8272 df-map 8391 df-ixp 8445 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-sup 8890 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-z 11970 df-dec 12087 df-uz 12232 df-rp 12378 df-fz 12886 df-seq 13365 df-exp 13426 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-starv 16572 df-sca 16573 df-vsca 16574 df-ip 16575 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-hom 16581 df-cco 16582 df-0g 16707 df-prds 16713 df-pws 16715 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-mhm 17948 df-grp 18098 df-minusg 18099 df-sbg 18100 df-subg 18268 df-ghm 18348 df-cmn 18900 df-mgp 19233 df-ur 19245 df-ring 19292 df-cring 19293 df-oppr 19369 df-dvdsr 19387 df-unit 19388 df-invr 19418 df-dvr 19429 df-rnghom 19463 df-drng 19497 df-field 19498 df-subrg 19526 df-staf 19609 df-srng 19610 df-lmod 19629 df-lss 19697 df-sra 19937 df-rgmod 19938 df-cnfld 20092 df-refld 20294 df-dsmm 20421 df-frlm 20436 df-tng 23191 df-tcph 23774 df-rrx 23989 df-line 45143

This theorem is referenced by: (None)

W3C validator