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 43316

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	⊢ 𝑃 = (ℝ ↑_𝑚 𝐼)
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 10359	. . . . . . . . . . 11 ⊢ 1 ∈ V
4		2ex 11435	. . . . . . . . . . 11 ⊢ 2 ∈ V
5	3, 4	pm3.2i 464	. . . . . . . . . 10 ⊢ (1 ∈ V ∧ 2 ∈ V)
6		c0ex 10357	. . . . . . . . . . 11 ⊢ 0 ∈ V
7	6	jctl 519	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (0 ∈ V ∧ 𝑀 ∈ ℝ))
8		1ne2 11573	. . . . . . . . . . 11 ⊢ 1 ≠ 2
9	8	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → 1 ≠ 2)
10		fprg 6678	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{0, 𝑀})
11		0red 10367	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ V ∧ 2 ∈ V) → 0 ∈ ℝ)
12		simpr 479	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ V ∧ 𝑀 ∈ ℝ) → 𝑀 ∈ ℝ)
13	11, 12	anim12i 606	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ)) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
14	13	3adant3 1166	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
15		prssi 4572	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {0, 𝑀} ⊆ ℝ)
16	14, 15	syl 17	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0, 𝑀} ⊆ ℝ)
17	10, 16	fssd 6296	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
18	5, 7, 9, 17	mp3an2i 1594	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
19		line2.i	. . . . . . . . . 10 ⊢ 𝐼 = {1, 2}
20	19	feq2i 6274	. . . . . . . . 9 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
21	18, 20	sylibr 226	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
22		reex 10350	. . . . . . . . 9 ⊢ ℝ ∈ V
23		prex 5132	. . . . . . . . . 10 ⊢ {1, 2} ∈ V
24	19, 23	eqeltri 2902	. . . . . . . . 9 ⊢ 𝐼 ∈ V
25	22, 24	elmap 8156	. . . . . . . 8 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_𝑚 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
26	21, 25	sylibr 226	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_𝑚 𝐼))
27		line2x.x	. . . . . . 7 ⊢ 𝑋 = {⟨1, 0⟩, ⟨2, 𝑀⟩}
28		line2.p	. . . . . . 7 ⊢ 𝑃 = (ℝ ↑_𝑚 𝐼)
29	26, 27, 28	3eltr4g 2923	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃)
30	3	jctl 519	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (1 ∈ V ∧ 𝑀 ∈ ℝ))
31		fprg 6678	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
32	5, 30, 9, 31	mp3an2i 1594	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
33		1re 10363	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
34		prssi 4572	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {1, 𝑀} ⊆ ℝ)
35	33, 34	mpan 681	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {1, 𝑀} ⊆ ℝ)
36	32, 35	fssd 6296	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
37	19	feq2i 6274	. . . . . . . . 9 ⊢ ({⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
38	36, 37	sylibr 226	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
39	22, 24	pm3.2i 464	. . . . . . . . 9 ⊢ (ℝ ∈ V ∧ 𝐼 ∈ V)
40		elmapg 8140	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ 𝐼 ∈ V) → ({⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_𝑚 𝐼) ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ))
41	39, 40	mp1i 13	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_𝑚 𝐼) ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ))
42	38, 41	mpbird 249	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_𝑚 𝐼))
43		line2x.y	. . . . . . 7 ⊢ 𝑌 = {⟨1, 1⟩, ⟨2, 𝑀⟩}
44	42, 43, 28	3eltr4g 2923	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑌 ∈ 𝑃)
45		opex 5155	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ∈ V
46		opex 5155	. . . . . . . . . 10 ⊢ ⟨2, 𝑀⟩ ∈ V
47	45, 46	pm3.2i 464	. . . . . . . . 9 ⊢ (⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
48		opex 5155	. . . . . . . . . 10 ⊢ ⟨1, 1⟩ ∈ V
49	48, 46	pm3.2i 464	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
50	47, 49	pm3.2i 464	. . . . . . . 8 ⊢ ((⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V) ∧ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V))
51	8	orci 896	. . . . . . . . . . . 12 ⊢ (1 ≠ 2 ∨ 0 ≠ 𝑀)
52	3, 6	opthne 5173	. . . . . . . . . . . 12 ⊢ (⟨1, 0⟩ ≠ ⟨2, 𝑀⟩ ↔ (1 ≠ 2 ∨ 0 ≠ 𝑀))
53	51, 52	mpbir 223	. . . . . . . . . . 11 ⊢ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩
54	53	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩)
55		0ne1 11429	. . . . . . . . . . . 12 ⊢ 0 ≠ 1
56	55	olci 897	. . . . . . . . . . 11 ⊢ (1 ≠ 1 ∨ 0 ≠ 1)
57	3, 6	opthne 5173	. . . . . . . . . . 11 ⊢ (⟨1, 0⟩ ≠ ⟨1, 1⟩ ↔ (1 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 223	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ≠ ⟨1, 1⟩
59	54, 58	jctil 515	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩))
60	59	orcd 904	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩) ∨ (⟨2, 𝑀⟩ ≠ ⟨1, 1⟩ ∧ ⟨2, 𝑀⟩ ≠ ⟨2, 𝑀⟩)))
61		prneimg 4605	. . . . . . . 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 3078	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ≠ 𝑌)
64	29, 44, 63	3jca 1162	. . . . 5 ⊢ (𝑀 ∈ ℝ → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
65	64	adantl 475	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
66		line2.e	. . . . 5 ⊢ 𝐸 = (ℝ^‘𝐼)
67		line2.l	. . . . 5 ⊢ 𝐿 = (Line_M‘𝐸)
68		eqid 2825	. . . . 5 ⊢ ((𝑌‘1) − (𝑋‘1)) = ((𝑌‘1) − (𝑋‘1))
69		eqid 2825	. . . . 5 ⊢ ((𝑌‘2) − (𝑋‘2)) = ((𝑌‘2) − (𝑋‘2))
70		eqid 2825	. . . . 5 ⊢ (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))
71	19, 66, 28, 67, 68, 69, 70	rrx2linest 43306	. . . 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 2840	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))}))
74		rabbi 3331	. . 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 6438	. . . . . . . . . . . . 13 ⊢ (𝑌‘1) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1)
76	3, 3, 8	3pm3.2i 1442	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2)
77		fvpr1g 6719	. . . . . . . . . . . . . 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 2873	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
80	27	fveq1i 6438	. . . . . . . . . . . . 13 ⊢ (𝑋‘1) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1)
81	3, 6, 8	3pm3.2i 1442	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2)
82		fvpr1g 6719	. . . . . . . . . . . . . 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 2873	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
85	79, 84	oveq12d 6928	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = (1 − 0))
86		1m0e1 11486	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
87	85, 86	syl6eq 2877	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = 1)
88	87	oveq1d 6925	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = (1 · (𝑝‘2)))
89	43	fveq1i 6438	. . . . . . . . . . . . . 14 ⊢ (𝑌‘2) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2)
90		fvpr2g 6720	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
91	4, 8, 90	mp3an13 1580	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
92	89, 91	syl5eq 2873	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑌‘2) = 𝑀)
93	27	fveq1i 6438	. . . . . . . . . . . . . 14 ⊢ (𝑋‘2) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2)
94		fvpr2g 6720	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
95	4, 8, 94	mp3an13 1580	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
96	93, 95	syl5eq 2873	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑋‘2) = 𝑀)
97	92, 96	oveq12d 6928	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = (𝑀 − 𝑀))
98		recn 10349	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → 𝑀 ∈ ℂ)
99	98	subidd 10708	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑀 − 𝑀) = 0)
100	97, 99	eqtrd 2861	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = 0)
101	100	oveq1d 6925	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = (0 · (𝑝‘1)))
102	3, 3, 9, 77	mp3an12i 1593	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
103	75, 102	syl5eq 2873	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
104	96, 103	oveq12d 6928	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = (𝑀 · 1))
105		ax-1rid 10329	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑀 · 1) = 𝑀)
106	104, 105	eqtrd 2861	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = 𝑀)
107	3, 6, 9, 82	mp3an12i 1593	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
108	80, 107	syl5eq 2873	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
109	108, 92	oveq12d 6928	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = (0 · 𝑀))
110	98	mul02d 10560	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (0 · 𝑀) = 0)
111	109, 110	eqtrd 2861	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = 0)
112	106, 111	oveq12d 6928	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (𝑀 − 0))
113	98	subid1d 10709	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 0) = 𝑀)
114	112, 113	eqtrd 2861	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = 𝑀)
115	101, 114	oveq12d 6928	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) = ((0 · (𝑝‘1)) + 𝑀))
116	88, 115	eqeq12d 2840	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
117	116	adantl 475	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
118	19, 28	rrx2pyel 42272	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ)
119	118	recnd 10392	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ)
120	119	mulid2d 10382	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → (1 · (𝑝‘2)) = (𝑝‘2))
121	19, 28	rrx2pxel 42271	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
122	121	recnd 10392	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
123	122	mul02d 10560	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘1)) = 0)
124	123	oveq1d 6925	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → ((0 · (𝑝‘1)) + 𝑀) = (0 + 𝑀))
125	120, 124	eqeq12d 2840	. . . . . . 7 ⊢ (𝑝 ∈ 𝑃 → ((1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀) ↔ (𝑝‘2) = (0 + 𝑀)))
126	117, 125	sylan9bb 505	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (𝑝‘2) = (0 + 𝑀)))
127	126	bibi2d 334	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
128	127	ralbidva 3194	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
129	98	addid2d 10563	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (0 + 𝑀) = 𝑀)
130	129	adantr 474	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → (0 + 𝑀) = 𝑀)
131	130	eqeq2d 2835	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (0 + 𝑀) ↔ (𝑝‘2) = 𝑀))
132	131	bibi2d 334	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
133	132	ralbidva 3194	. . . . 5 ⊢ (𝑀 ∈ ℝ → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
134	133	adantl 475	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
135	19, 66, 28, 67, 1, 27, 43	line2xlem 43315	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) → (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
136		oveq1 6917	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
137	136	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
138	137	ad2antlr 718	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
139	123	adantl 475	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 · (𝑝‘1)) = 0)
140	138, 139	eqtrd 2861	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = 0)
141	140	oveq1d 6925	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (0 + (𝐵 · (𝑝‘2))))
142		recn 10349	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
143	142	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
144	143	3ad2ant2 1168	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
145	144	ad3antrrr 721	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
146	119	adantl 475	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℂ)
147	145, 146	mulcld 10384	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ)
148	147	addid2d 10563	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
149	141, 148	eqtrd 2861	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
150	149	eqeq1d 2827	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝐵 · (𝑝‘2)) = 𝐶))
151		simp3 1172	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
152	151	recnd 10392	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
153	152	ad3antrrr 721	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ)
154		simpl 476	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℝ)
155	154	recnd 10392	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
156	155	3ad2ant2 1168	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
157	156	ad3antrrr 721	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
158		simp2r 1261	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ≠ 0)
159	158	ad3antrrr 721	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ≠ 0)
160	153, 157, 146, 159	divmuld 11156	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ (𝐵 · (𝑝‘2)) = 𝐶))
161		simpr 479	. . . . . . . . . . . 12 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → 𝑀 = (𝐶 / 𝐵))
162	161	eqcomd 2831	. . . . . . . . . . 11 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐶 / 𝐵) = 𝑀)
163	162	ad2antlr 718	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) = 𝑀)
164	163	eqeq1d 2827	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ 𝑀 = (𝑝‘2)))
165	150, 160, 164	3bitr2d 299	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ 𝑀 = (𝑝‘2)))
166		eqcom 2832	. . . . . . . 8 ⊢ (𝑀 = (𝑝‘2) ↔ (𝑝‘2) = 𝑀)
167	165, 166	syl6bb 279	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
168	167	ralrimiva 3175	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
169	168	ex 403	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
170	135, 169	impbid 204	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
171	128, 134, 170	3bitrd 297	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
172	74, 171	syl5bbr 277	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))} ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
173	73, 172	bitrd 271	1 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 878 ∧ w3a 1111 = wceq 1656 ∈ wcel 2164 ≠ wne 2999 ∀wral 3117 {crab 3121 Vcvv 3414 ⊆ wss 3798 {cpr 4401 ⟨cop 4405 ⟶wf 6123 ‘cfv 6127 (class class class)co 6910 ↑_𝑚 cmap 8127 ℂcc 10257 ℝcr 10258 0cc0 10259 1c1 10260 + caddc 10262 · cmul 10264 − cmin 10592 / cdiv 11016 2c2 11413 ℝ^crrx 23558 Line_Mcline 43291

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-rep 4996 ax-sep 5007 ax-nul 5015 ax-pow 5067 ax-pr 5129 ax-un 7214 ax-cnex 10315 ax-resscn 10316 ax-1cn 10317 ax-icn 10318 ax-addcl 10319 ax-addrcl 10320 ax-mulcl 10321 ax-mulrcl 10322 ax-mulcom 10323 ax-addass 10324 ax-mulass 10325 ax-distr 10326 ax-i2m1 10327 ax-1ne0 10328 ax-1rid 10329 ax-rnegex 10330 ax-rrecex 10331 ax-cnre 10332 ax-pre-lttri 10333 ax-pre-lttrn 10334 ax-pre-ltadd 10335 ax-pre-mulgt0 10336 ax-pre-sup 10337 ax-addf 10338 ax-mulf 10339

This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-nel 3103 df-ral 3122 df-rex 3123 df-reu 3124 df-rmo 3125 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-pss 3814 df-nul 4147 df-if 4309 df-pw 4382 df-sn 4400 df-pr 4402 df-tp 4404 df-op 4406 df-uni 4661 df-int 4700 df-iun 4744 df-br 4876 df-opab 4938 df-mpt 4955 df-tr 4978 df-id 5252 df-eprel 5257 df-po 5265 df-so 5266 df-fr 5305 df-we 5307 df-xp 5352 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-rn 5357 df-res 5358 df-ima 5359 df-pred 5924 df-ord 5970 df-on 5971 df-lim 5972 df-suc 5973 df-iota 6090 df-fun 6129 df-fn 6130 df-f 6131 df-f1 6132 df-fo 6133 df-f1o 6134 df-fv 6135 df-riota 6871 df-ov 6913 df-oprab 6914 df-mpt2 6915 df-of 7162 df-om 7332 df-1st 7433 df-2nd 7434 df-supp 7565 df-tpos 7622 df-wrecs 7677 df-recs 7739 df-rdg 7777 df-1o 7831 df-oadd 7835 df-er 8014 df-map 8129 df-ixp 8182 df-en 8229 df-dom 8230 df-sdom 8231 df-fin 8232 df-fsupp 8551 df-sup 8623 df-pnf 10400 df-mnf 10401 df-xr 10402 df-ltxr 10403 df-le 10404 df-sub 10594 df-neg 10595 df-div 11017 df-nn 11358 df-2 11421 df-3 11422 df-4 11423 df-5 11424 df-6 11425 df-7 11426 df-8 11427 df-9 11428 df-n0 11626 df-z 11712 df-dec 11829 df-uz 11976 df-rp 12120 df-fz 12627 df-seq 13103 df-exp 13162 df-cj 14223 df-re 14224 df-im 14225 df-sqrt 14359 df-abs 14360 df-struct 16231 df-ndx 16232 df-slot 16233 df-base 16235 df-sets 16236 df-ress 16237 df-plusg 16325 df-mulr 16326 df-starv 16327 df-sca 16328 df-vsca 16329 df-ip 16330 df-tset 16331 df-ple 16332 df-ds 16334 df-unif 16335 df-hom 16336 df-cco 16337 df-0g 16462 df-prds 16468 df-pws 16470 df-mgm 17602 df-sgrp 17644 df-mnd 17655 df-mhm 17695 df-grp 17786 df-minusg 17787 df-sbg 17788 df-subg 17949 df-ghm 18016 df-cmn 18555 df-mgp 18851 df-ur 18863 df-ring 18910 df-cring 18911 df-oppr 18984 df-dvdsr 19002 df-unit 19003 df-invr 19033 df-dvr 19044 df-rnghom 19078 df-drng 19112 df-field 19113 df-subrg 19141 df-staf 19208 df-srng 19209 df-lmod 19228 df-lss 19296 df-sra 19540 df-rgmod 19541 df-cnfld 20114 df-refld 20319 df-dsmm 20446 df-frlm 20461 df-tng 22766 df-tcph 23345 df-rrx 23560 df-line 43293

This theorem is referenced by: (None)

W3C validator