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 48648

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 11239	. . . . . . . . . . 11 ⊢ 1 ∈ V
4		2ex 12325	. . . . . . . . . . 11 ⊢ 2 ∈ V
5	3, 4	pm3.2i 470	. . . . . . . . . 10 ⊢ (1 ∈ V ∧ 2 ∈ V)
6		c0ex 11237	. . . . . . . . . . 11 ⊢ 0 ∈ V
7	6	jctl 523	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (0 ∈ V ∧ 𝑀 ∈ ℝ))
8		1ne2 12456	. . . . . . . . . . 11 ⊢ 1 ≠ 2
9	8	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → 1 ≠ 2)
10		fprg 7155	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{0, 𝑀})
11		0red 11246	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ V ∧ 2 ∈ V) → 0 ∈ ℝ)
12		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ V ∧ 𝑀 ∈ ℝ) → 𝑀 ∈ ℝ)
13	11, 12	anim12i 613	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ)) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
14	13	3adant3 1132	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
15		prssi 4801	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {0, 𝑀} ⊆ ℝ)
16	14, 15	syl 17	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0, 𝑀} ⊆ ℝ)
17	10, 16	fssd 6733	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
18	5, 7, 9, 17	mp3an2i 1467	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
19		line2.i	. . . . . . . . . 10 ⊢ 𝐼 = {1, 2}
20	19	feq2i 6708	. . . . . . . . 9 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
21	18, 20	sylibr 234	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
22		reex 11228	. . . . . . . . 9 ⊢ ℝ ∈ V
23		prex 5417	. . . . . . . . . 10 ⊢ {1, 2} ∈ V
24	19, 23	eqeltri 2829	. . . . . . . . 9 ⊢ 𝐼 ∈ V
25	22, 24	elmap 8893	. . . . . . . 8 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
26	21, 25	sylibr 234	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼))
27		line2x.x	. . . . . . 7 ⊢ 𝑋 = {⟨1, 0⟩, ⟨2, 𝑀⟩}
28		line2.p	. . . . . . 7 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
29	26, 27, 28	3eltr4g 2850	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃)
30	3	jctl 523	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (1 ∈ V ∧ 𝑀 ∈ ℝ))
31		fprg 7155	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
32	5, 30, 9, 31	mp3an2i 1467	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
33		1re 11243	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
34		prssi 4801	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {1, 𝑀} ⊆ ℝ)
35	33, 34	mpan 690	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {1, 𝑀} ⊆ ℝ)
36	32, 35	fssd 6733	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
37	19	feq2i 6708	. . . . . . . . 9 ⊢ ({⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
38	36, 37	sylibr 234	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
39	22, 24	pm3.2i 470	. . . . . . . . 9 ⊢ (ℝ ∈ V ∧ 𝐼 ∈ V)
40		elmapg 8861	. . . . . . . . 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 257	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼))
43		line2x.y	. . . . . . 7 ⊢ 𝑌 = {⟨1, 1⟩, ⟨2, 𝑀⟩}
44	42, 43, 28	3eltr4g 2850	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑌 ∈ 𝑃)
45		opex 5449	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ∈ V
46		opex 5449	. . . . . . . . . 10 ⊢ ⟨2, 𝑀⟩ ∈ V
47	45, 46	pm3.2i 470	. . . . . . . . 9 ⊢ (⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
48		opex 5449	. . . . . . . . . 10 ⊢ ⟨1, 1⟩ ∈ V
49	48, 46	pm3.2i 470	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
50	47, 49	pm3.2i 470	. . . . . . . 8 ⊢ ((⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V) ∧ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V))
51	8	orci 865	. . . . . . . . . . . 12 ⊢ (1 ≠ 2 ∨ 0 ≠ 𝑀)
52	3, 6	opthne 5467	. . . . . . . . . . . 12 ⊢ (⟨1, 0⟩ ≠ ⟨2, 𝑀⟩ ↔ (1 ≠ 2 ∨ 0 ≠ 𝑀))
53	51, 52	mpbir 231	. . . . . . . . . . 11 ⊢ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩
54	53	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩)
55		0ne1 12319	. . . . . . . . . . . 12 ⊢ 0 ≠ 1
56	55	olci 866	. . . . . . . . . . 11 ⊢ (1 ≠ 1 ∨ 0 ≠ 1)
57	3, 6	opthne 5467	. . . . . . . . . . 11 ⊢ (⟨1, 0⟩ ≠ ⟨1, 1⟩ ↔ (1 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 231	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ≠ ⟨1, 1⟩
59	54, 58	jctil 519	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩))
60	59	orcd 873	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩) ∨ (⟨2, 𝑀⟩ ≠ ⟨1, 1⟩ ∧ ⟨2, 𝑀⟩ ≠ ⟨2, 𝑀⟩)))
61		prneimg 4834	. . . . . . . 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 3010	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ≠ 𝑌)
64	29, 44, 63	3jca 1128	. . . . 5 ⊢ (𝑀 ∈ ℝ → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
65	64	adantl 481	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
66		line2.e	. . . . 5 ⊢ 𝐸 = (ℝ^‘𝐼)
67		line2.l	. . . . 5 ⊢ 𝐿 = (Line_M‘𝐸)
68		eqid 2734	. . . . 5 ⊢ ((𝑌‘1) − (𝑋‘1)) = ((𝑌‘1) − (𝑋‘1))
69		eqid 2734	. . . . 5 ⊢ ((𝑌‘2) − (𝑋‘2)) = ((𝑌‘2) − (𝑋‘2))
70		eqid 2734	. . . . 5 ⊢ (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))
71	19, 66, 28, 67, 68, 69, 70	rrx2linest 48636	. . . 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 2750	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))}))
74		rabbi 3450	. . 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 6887	. . . . . . . . . . . . 13 ⊢ (𝑌‘1) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1)
76	3, 3, 8	3pm3.2i 1339	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2)
77		fvpr1g 7192	. . . . . . . . . . . . . 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	eqtrid 2781	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
80	27	fveq1i 6887	. . . . . . . . . . . . 13 ⊢ (𝑋‘1) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1)
81	3, 6, 8	3pm3.2i 1339	. . . . . . . . . . . . . 14 ⊢ (1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2)
82		fvpr1g 7192	. . . . . . . . . . . . . 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	eqtrid 2781	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
85	79, 84	oveq12d 7431	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = (1 − 0))
86		1m0e1 12369	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
87	85, 86	eqtrdi 2785	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = 1)
88	87	oveq1d 7428	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = (1 · (𝑝‘2)))
89	43	fveq1i 6887	. . . . . . . . . . . . . 14 ⊢ (𝑌‘2) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2)
90		fvpr2g 7193	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
91	4, 8, 90	mp3an13 1453	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
92	89, 91	eqtrid 2781	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑌‘2) = 𝑀)
93	27	fveq1i 6887	. . . . . . . . . . . . . 14 ⊢ (𝑋‘2) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2)
94		fvpr2g 7193	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
95	4, 8, 94	mp3an13 1453	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
96	93, 95	eqtrid 2781	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑋‘2) = 𝑀)
97	92, 96	oveq12d 7431	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = (𝑀 − 𝑀))
98		recn 11227	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → 𝑀 ∈ ℂ)
99	98	subidd 11590	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑀 − 𝑀) = 0)
100	97, 99	eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = 0)
101	100	oveq1d 7428	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = (0 · (𝑝‘1)))
102	3, 3, 9, 77	mp3an12i 1466	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
103	75, 102	eqtrid 2781	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
104	96, 103	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = (𝑀 · 1))
105		ax-1rid 11207	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑀 · 1) = 𝑀)
106	104, 105	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = 𝑀)
107	3, 6, 9, 82	mp3an12i 1466	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
108	80, 107	eqtrid 2781	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
109	108, 92	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = (0 · 𝑀))
110	98	mul02d 11441	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (0 · 𝑀) = 0)
111	109, 110	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = 0)
112	106, 111	oveq12d 7431	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (𝑀 − 0))
113	98	subid1d 11591	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 0) = 𝑀)
114	112, 113	eqtrd 2769	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = 𝑀)
115	101, 114	oveq12d 7431	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) = ((0 · (𝑝‘1)) + 𝑀))
116	88, 115	eqeq12d 2750	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
117	116	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
118	19, 28	rrx2pyel 48606	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ)
119	118	recnd 11271	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ)
120	119	mullidd 11261	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → (1 · (𝑝‘2)) = (𝑝‘2))
121	19, 28	rrx2pxel 48605	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
122	121	recnd 11271	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
123	122	mul02d 11441	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘1)) = 0)
124	123	oveq1d 7428	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → ((0 · (𝑝‘1)) + 𝑀) = (0 + 𝑀))
125	120, 124	eqeq12d 2750	. . . . . . 7 ⊢ (𝑝 ∈ 𝑃 → ((1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀) ↔ (𝑝‘2) = (0 + 𝑀)))
126	117, 125	sylan9bb 509	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (𝑝‘2) = (0 + 𝑀)))
127	126	bibi2d 342	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
128	127	ralbidva 3163	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
129	98	addlidd 11444	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (0 + 𝑀) = 𝑀)
130	129	adantr 480	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → (0 + 𝑀) = 𝑀)
131	130	eqeq2d 2745	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (0 + 𝑀) ↔ (𝑝‘2) = 𝑀))
132	131	bibi2d 342	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
133	132	ralbidva 3163	. . . . 5 ⊢ (𝑀 ∈ ℝ → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
134	133	adantl 481	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
135	19, 66, 28, 67, 1, 27, 43	line2xlem 48647	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) → (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
136		oveq1 7420	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
137	136	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
138	137	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
139	123	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 · (𝑝‘1)) = 0)
140	138, 139	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = 0)
141	140	oveq1d 7428	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (0 + (𝐵 · (𝑝‘2))))
142		recn 11227	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
143	142	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
144	143	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
145	144	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
146	119	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℂ)
147	145, 146	mulcld 11263	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ)
148	147	addlidd 11444	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
149	141, 148	eqtrd 2769	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
150	149	eqeq1d 2736	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝐵 · (𝑝‘2)) = 𝐶))
151		simp3 1138	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
152	151	recnd 11271	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
153	152	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ)
154		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℝ)
155	154	recnd 11271	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
156	155	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
157	156	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
158		simp2r 1200	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ≠ 0)
159	158	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ≠ 0)
160	153, 157, 146, 159	divmuld 12047	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ (𝐵 · (𝑝‘2)) = 𝐶))
161		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → 𝑀 = (𝐶 / 𝐵))
162	161	eqcomd 2740	. . . . . . . . . . 11 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐶 / 𝐵) = 𝑀)
163	162	ad2antlr 727	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) = 𝑀)
164	163	eqeq1d 2736	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ 𝑀 = (𝑝‘2)))
165	150, 160, 164	3bitr2d 307	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ 𝑀 = (𝑝‘2)))
166		eqcom 2741	. . . . . . . 8 ⊢ (𝑀 = (𝑝‘2) ↔ (𝑝‘2) = 𝑀)
167	165, 166	bitrdi 287	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
168	167	ralrimiva 3133	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
169	168	ex 412	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
170	135, 169	impbid 212	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
171	128, 134, 170	3bitrd 305	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
172	74, 171	bitr3id 285	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))} ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
173	73, 172	bitrd 279	1 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 {crab 3419 Vcvv 3463 ⊆ wss 3931 {cpr 4608 ⟨cop 4612 ⟶wf 6537 ‘cfv 6541 (class class class)co 7413 ↑_m cmap 8848 ℂcc 11135 ℝcr 11136 0cc0 11137 1c1 11138 + caddc 11140 · cmul 11142 − cmin 11474 / cdiv 11902 2c2 12303 ℝ^crrx 25354 Line_Mcline 48621

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 ax-addf 11216 ax-mulf 11217

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-iun 4973 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-om 7870 df-1st 7996 df-2nd 7997 df-supp 8168 df-tpos 8233 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-er 8727 df-map 8850 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fsupp 9384 df-sup 9464 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-z 12597 df-dec 12717 df-uz 12861 df-rp 13017 df-fz 13530 df-seq 14025 df-exp 14085 df-cj 15121 df-re 15122 df-im 15123 df-sqrt 15257 df-abs 15258 df-struct 17167 df-sets 17184 df-slot 17202 df-ndx 17214 df-base 17231 df-ress 17254 df-plusg 17287 df-mulr 17288 df-starv 17289 df-sca 17290 df-vsca 17291 df-ip 17292 df-tset 17293 df-ple 17294 df-ds 17296 df-unif 17297 df-hom 17298 df-cco 17299 df-0g 17458 df-prds 17464 df-pws 17466 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-mhm 18766 df-grp 18924 df-minusg 18925 df-sbg 18926 df-subg 19111 df-ghm 19201 df-cmn 19769 df-abl 19770 df-mgp 20107 df-rng 20119 df-ur 20148 df-ring 20201 df-cring 20202 df-oppr 20303 df-dvdsr 20326 df-unit 20327 df-invr 20357 df-dvr 20370 df-rhm 20441 df-subrng 20515 df-subrg 20539 df-drng 20700 df-field 20701 df-staf 20809 df-srng 20810 df-lmod 20829 df-lss 20899 df-sra 21141 df-rgmod 21142 df-cnfld 21328 df-refld 21578 df-dsmm 21707 df-frlm 21722 df-tng 24542 df-tcph 25140 df-rrx 25356 df-line 48623

This theorem is referenced by: (None)

W3C validator