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 45533

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 10675	. . . . . . . . . . 11 ⊢ 1 ∈ V
4		2ex 11751	. . . . . . . . . . 11 ⊢ 2 ∈ V
5	3, 4	pm3.2i 474	. . . . . . . . . 10 ⊢ (1 ∈ V ∧ 2 ∈ V)
6		c0ex 10673	. . . . . . . . . . 11 ⊢ 0 ∈ V
7	6	jctl 527	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (0 ∈ V ∧ 𝑀 ∈ ℝ))
8		1ne2 11882	. . . . . . . . . . 11 ⊢ 1 ≠ 2
9	8	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → 1 ≠ 2)
10		fprg 6908	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{0, 𝑀})
11		0red 10682	. . . . . . . . . . . . . 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 4711	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {0, 𝑀} ⊆ ℝ)
16	14, 15	syl 17	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0, 𝑀} ⊆ ℝ)
17	10, 16	fssd 6513	. . . . . . . . . 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 6490	. . . . . . . . 9 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
21	18, 20	sylibr 237	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
22		reex 10666	. . . . . . . . 9 ⊢ ℝ ∈ V
23		prex 5301	. . . . . . . . . 10 ⊢ {1, 2} ∈ V
24	19, 23	eqeltri 2848	. . . . . . . . 9 ⊢ 𝐼 ∈ V
25	22, 24	elmap 8453	. . . . . . . 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 2869	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃)
30	3	jctl 527	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (1 ∈ V ∧ 𝑀 ∈ ℝ))
31		fprg 6908	. . . . . . . . . . 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 10679	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
34		prssi 4711	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {1, 𝑀} ⊆ ℝ)
35	33, 34	mpan 689	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {1, 𝑀} ⊆ ℝ)
36	32, 35	fssd 6513	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
37	19	feq2i 6490	. . . . . . . . 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 8429	. . . . . . . . 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 2869	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑌 ∈ 𝑃)
45		opex 5324	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ∈ V
46		opex 5324	. . . . . . . . . 10 ⊢ ⟨2, 𝑀⟩ ∈ V
47	45, 46	pm3.2i 474	. . . . . . . . 9 ⊢ (⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
48		opex 5324	. . . . . . . . . 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 5342	. . . . . . . . . . . 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 11745	. . . . . . . . . . . 12 ⊢ 0 ≠ 1
56	55	olci 863	. . . . . . . . . . 11 ⊢ (1 ≠ 1 ∨ 0 ≠ 1)
57	3, 6	opthne 5342	. . . . . . . . . . 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 4742	. . . . . . . 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 3030	. . . . . 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 2758	. . . . 5 ⊢ ((𝑌‘1) − (𝑋‘1)) = ((𝑌‘1) − (𝑋‘1))
69		eqid 2758	. . . . 5 ⊢ ((𝑌‘2) − (𝑋‘2)) = ((𝑌‘2) − (𝑋‘2))
70		eqid 2758	. . . . 5 ⊢ (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))
71	19, 66, 28, 67, 68, 69, 70	rrx2linest 45521	. . . 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 2774	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))}))
74		rabbi 3301	. . 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 6659	. . . . . . . . . . . . 13 ⊢ (𝑌‘1) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1)
76	3, 3, 8	3pm3.2i 1336	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2)
77		fvpr1g 6945	. . . . . . . . . . . . . 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 2805	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
80	27	fveq1i 6659	. . . . . . . . . . . . 13 ⊢ (𝑋‘1) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1)
81	3, 6, 8	3pm3.2i 1336	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2)
82		fvpr1g 6945	. . . . . . . . . . . . . 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 2805	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
85	79, 84	oveq12d 7168	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = (1 − 0))
86		1m0e1 11795	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
87	85, 86	eqtrdi 2809	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = 1)
88	87	oveq1d 7165	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = (1 · (𝑝‘2)))
89	43	fveq1i 6659	. . . . . . . . . . . . . 14 ⊢ (𝑌‘2) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2)
90		fvpr2g 6946	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
91	4, 8, 90	mp3an13 1449	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
92	89, 91	syl5eq 2805	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑌‘2) = 𝑀)
93	27	fveq1i 6659	. . . . . . . . . . . . . 14 ⊢ (𝑋‘2) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2)
94		fvpr2g 6946	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
95	4, 8, 94	mp3an13 1449	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
96	93, 95	syl5eq 2805	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑋‘2) = 𝑀)
97	92, 96	oveq12d 7168	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = (𝑀 − 𝑀))
98		recn 10665	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → 𝑀 ∈ ℂ)
99	98	subidd 11023	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑀 − 𝑀) = 0)
100	97, 99	eqtrd 2793	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = 0)
101	100	oveq1d 7165	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = (0 · (𝑝‘1)))
102	3, 3, 9, 77	mp3an12i 1462	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
103	75, 102	syl5eq 2805	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
104	96, 103	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = (𝑀 · 1))
105		ax-1rid 10645	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑀 · 1) = 𝑀)
106	104, 105	eqtrd 2793	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = 𝑀)
107	3, 6, 9, 82	mp3an12i 1462	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
108	80, 107	syl5eq 2805	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
109	108, 92	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = (0 · 𝑀))
110	98	mul02d 10876	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (0 · 𝑀) = 0)
111	109, 110	eqtrd 2793	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = 0)
112	106, 111	oveq12d 7168	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (𝑀 − 0))
113	98	subid1d 11024	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 0) = 𝑀)
114	112, 113	eqtrd 2793	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = 𝑀)
115	101, 114	oveq12d 7168	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) = ((0 · (𝑝‘1)) + 𝑀))
116	88, 115	eqeq12d 2774	. . . . . . . 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 45491	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ)
119	118	recnd 10707	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ)
120	119	mulid2d 10697	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → (1 · (𝑝‘2)) = (𝑝‘2))
121	19, 28	rrx2pxel 45490	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
122	121	recnd 10707	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
123	122	mul02d 10876	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘1)) = 0)
124	123	oveq1d 7165	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → ((0 · (𝑝‘1)) + 𝑀) = (0 + 𝑀))
125	120, 124	eqeq12d 2774	. . . . . . 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 3125	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
129	98	addid2d 10879	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (0 + 𝑀) = 𝑀)
130	129	adantr 484	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → (0 + 𝑀) = 𝑀)
131	130	eqeq2d 2769	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (0 + 𝑀) ↔ (𝑝‘2) = 𝑀))
132	131	bibi2d 346	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
133	132	ralbidva 3125	. . . . 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 45532	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) → (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
136		oveq1 7157	. . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = 0)
141	140	oveq1d 7165	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (0 + (𝐵 · (𝑝‘2))))
142		recn 10665	. . . . . . . . . . . . . . . 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 10699	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ)
148	147	addid2d 10879	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
149	141, 148	eqtrd 2793	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
150	149	eqeq1d 2760	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝐵 · (𝑝‘2)) = 𝐶))
151		simp3 1135	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
152	151	recnd 10707	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
153	152	ad3antrrr 729	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ)
154		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℝ)
155	154	recnd 10707	. . . . . . . . . . . 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 11476	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ (𝐵 · (𝑝‘2)) = 𝐶))
161		simpr 488	. . . . . . . . . . . 12 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → 𝑀 = (𝐶 / 𝐵))
162	161	eqcomd 2764	. . . . . . . . . . 11 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐶 / 𝐵) = 𝑀)
163	162	ad2antlr 726	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) = 𝑀)
164	163	eqeq1d 2760	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ 𝑀 = (𝑝‘2)))
165	150, 160, 164	3bitr2d 310	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ 𝑀 = (𝑝‘2)))
166		eqcom 2765	. . . . . . . 8 ⊢ (𝑀 = (𝑝‘2) ↔ (𝑝‘2) = 𝑀)
167	165, 166	bitrdi 290	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
168	167	ralrimiva 3113	. . . . . 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 2951 ∀wral 3070 {crab 3074 Vcvv 3409 ⊆ wss 3858 {cpr 4524 ⟨cop 4528 ⟶wf 6331 ‘cfv 6335 (class class class)co 7150 ↑_m cmap 8416 ℂcc 10573 ℝcr 10574 0cc0 10575 1c1 10576 + caddc 10578 · cmul 10580 − cmin 10908 / cdiv 11335 2c2 11729 ℝ^crrx 24083 Line_Mcline 45506

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 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-pre-sup 10653 ax-addf 10654 ax-mulf 10655

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-iun 4885 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7405 df-om 7580 df-1st 7693 df-2nd 7694 df-supp 7836 df-tpos 7902 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-er 8299 df-map 8418 df-ixp 8480 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-fsupp 8867 df-sup 8939 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-div 11336 df-nn 11675 df-2 11737 df-3 11738 df-4 11739 df-5 11740 df-6 11741 df-7 11742 df-8 11743 df-9 11744 df-n0 11935 df-z 12021 df-dec 12138 df-uz 12283 df-rp 12431 df-fz 12940 df-seq 13419 df-exp 13480 df-cj 14506 df-re 14507 df-im 14508 df-sqrt 14642 df-abs 14643 df-struct 16543 df-ndx 16544 df-slot 16545 df-base 16547 df-sets 16548 df-ress 16549 df-plusg 16636 df-mulr 16637 df-starv 16638 df-sca 16639 df-vsca 16640 df-ip 16641 df-tset 16642 df-ple 16643 df-ds 16645 df-unif 16646 df-hom 16647 df-cco 16648 df-0g 16773 df-prds 16779 df-pws 16781 df-mgm 17918 df-sgrp 17967 df-mnd 17978 df-mhm 18022 df-grp 18172 df-minusg 18173 df-sbg 18174 df-subg 18343 df-ghm 18423 df-cmn 18975 df-mgp 19308 df-ur 19320 df-ring 19367 df-cring 19368 df-oppr 19444 df-dvdsr 19462 df-unit 19463 df-invr 19493 df-dvr 19504 df-rnghom 19538 df-drng 19572 df-field 19573 df-subrg 19601 df-staf 19684 df-srng 19685 df-lmod 19704 df-lss 19772 df-sra 20012 df-rgmod 20013 df-cnfld 20167 df-refld 20370 df-dsmm 20497 df-frlm 20512 df-tng 23286 df-tcph 23870 df-rrx 24085 df-line 45508

This theorem is referenced by: (None)

W3C validator