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 49692

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 11231	. . . . . . . . . . 11 ⊢ 1 ∈ V
4		2ex 12346	. . . . . . . . . . 11 ⊢ 2 ∈ V
5	3, 4	pm3.2i 476	. . . . . . . . . 10 ⊢ (1 ∈ V ∧ 2 ∈ V)
6		c0ex 11228	. . . . . . . . . . 11 ⊢ 0 ∈ V
7	6	jctl 533	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (0 ∈ V ∧ 𝑀 ∈ ℝ))
8		1ne2 12479	. . . . . . . . . . 11 ⊢ 1 ≠ 2
9	8	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → 1 ≠ 2)
10		fprg 7156	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{0, 𝑀})
11		0red 11239	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ V ∧ 2 ∈ V) → 0 ∈ ℝ)
12		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ V ∧ 𝑀 ∈ ℝ) → 𝑀 ∈ ℝ)
13	11, 12	anim12i 625	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ)) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
14	13	3adant3 1150	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ))
15		prssi 4785	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {0, 𝑀} ⊆ ℝ)
16	14, 15	syl 18	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0, 𝑀} ⊆ ℝ)
17	10, 16	fssd 6724	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
18	5, 7, 9, 17	mp3an2i 1495	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
19		line2.i	. . . . . . . . . 10 ⊢ 𝐼 = {1, 2}
20	19	feq2i 6698	. . . . . . . . 9 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
21	18, 20	sylibr 237	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
22		reex 11219	. . . . . . . . 9 ⊢ ℝ ∈ V
23		prex 5407	. . . . . . . . . 10 ⊢ {1, 2} ∈ V
24	19, 23	eqeltri 2858	. . . . . . . . 9 ⊢ 𝐼 ∈ V
25	22, 24	elmap 8882	. . . . . . . 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 2879	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃)
30	3	jctl 533	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (1 ∈ V ∧ 𝑀 ∈ ℝ))
31		fprg 7156	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
32	5, 30, 9, 31	mp3an2i 1495	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{1, 𝑀})
33		1re 11236	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
34		prssi 4785	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → {1, 𝑀} ⊆ ℝ)
35	33, 34	mpan 703	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {1, 𝑀} ⊆ ℝ)
36	32, 35	fssd 6724	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
37	19	feq2i 6698	. . . . . . . . 9 ⊢ ({⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
38	36, 37	sylibr 237	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
39	22, 24	pm3.2i 476	. . . . . . . . 9 ⊢ (ℝ ∈ V ∧ 𝐼 ∈ V)
40		elmapg 8842	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ 𝐼 ∈ V) → ({⟨1, 1⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 1⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ))
41	39, 40	mp1i 14	. . . . . . . 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 2879	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑌 ∈ 𝑃)
45		opex 5443	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ∈ V
46		opex 5443	. . . . . . . . . 10 ⊢ ⟨2, 𝑀⟩ ∈ V
47	45, 46	pm3.2i 476	. . . . . . . . 9 ⊢ (⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
48		opex 5443	. . . . . . . . . 10 ⊢ ⟨1, 1⟩ ∈ V
49	48, 46	pm3.2i 476	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V)
50	47, 49	pm3.2i 476	. . . . . . . 8 ⊢ ((⟨1, 0⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V) ∧ (⟨1, 1⟩ ∈ V ∧ ⟨2, 𝑀⟩ ∈ V))
51	8	orci 879	. . . . . . . . . . . 12 ⊢ (1 ≠ 2 ∨ 0 ≠ 𝑀)
52	3, 6	opthne 5462	. . . . . . . . . . . 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 12340	. . . . . . . . . . . 12 ⊢ 0 ≠ 1
56	55	olci 880	. . . . . . . . . . 11 ⊢ (1 ≠ 1 ∨ 0 ≠ 1)
57	3, 6	opthne 5462	. . . . . . . . . . 11 ⊢ (⟨1, 0⟩ ≠ ⟨1, 1⟩ ↔ (1 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 234	. . . . . . . . . 10 ⊢ ⟨1, 0⟩ ≠ ⟨1, 1⟩
59	54, 58	jctil 529	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩))
60	59	orcd 887	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((⟨1, 0⟩ ≠ ⟨1, 1⟩ ∧ ⟨1, 0⟩ ≠ ⟨2, 𝑀⟩) ∨ (⟨2, 𝑀⟩ ≠ ⟨1, 1⟩ ∧ ⟨2, 𝑀⟩ ≠ ⟨2, 𝑀⟩)))
61		prneimg 4817	. . . . . . . 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 69	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩} ≠ {⟨1, 1⟩, ⟨2, 𝑀⟩})
63	62, 27, 43	3netr4g 3036	. . . . . 6 ⊢ (𝑀 ∈ ℝ → 𝑋 ≠ 𝑌)
64	29, 44, 63	3jca 1146	. . . . 5 ⊢ (𝑀 ∈ ℝ → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
65	64	adantl 487	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌))
66		line2.e	. . . . 5 ⊢ 𝐸 = (ℝ^‘𝐼)
67		line2.l	. . . . 5 ⊢ 𝐿 = (Line_M‘𝐸)
68		eqid 2762	. . . . 5 ⊢ ((𝑌‘1) − (𝑋‘1)) = ((𝑌‘1) − (𝑋‘1))
69		eqid 2762	. . . . 5 ⊢ ((𝑌‘2) − (𝑋‘2)) = ((𝑌‘2) − (𝑋‘2))
70		eqid 2762	. . . . 5 ⊢ (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))
71	19, 66, 28, 67, 68, 69, 70	rrx2linest 49680	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))})
72	65, 71	syl 18	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))})
73	2, 72	eqeq12d 2778	. 2 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))}))
74		rabbi 3444	. . 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 6883	. . . . . . . . . . . . 13 ⊢ (𝑌‘1) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1)
76	3, 3, 8	3pm3.2i 1358	. . . . . . . . . . . . . 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 14	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
79	75, 78	eqtrid 2809	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
80	27	fveq1i 6883	. . . . . . . . . . . . 13 ⊢ (𝑋‘1) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1)
81	3, 6, 8	3pm3.2i 1358	. . . . . . . . . . . . . 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 14	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
84	80, 83	eqtrid 2809	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
85	79, 84	oveq12d 7435	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = (1 − 0))
86		1m0e1 12388	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
87	85, 86	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → ((𝑌‘1) − (𝑋‘1)) = 1)
88	87	oveq1d 7432	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = (1 · (𝑝‘2)))
89	43	fveq1i 6883	. . . . . . . . . . . . . 14 ⊢ (𝑌‘2) = ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2)
90		fvpr2g 7193	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
91	4, 8, 90	mp3an13 1481	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
92	89, 91	eqtrid 2809	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑌‘2) = 𝑀)
93	27	fveq1i 6883	. . . . . . . . . . . . . 14 ⊢ (𝑋‘2) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2)
94		fvpr2g 7193	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
95	4, 8, 94	mp3an13 1481	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
96	93, 95	eqtrid 2809	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑋‘2) = 𝑀)
97	92, 96	oveq12d 7435	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = (𝑀 − 𝑀))
98		recn 11218	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → 𝑀 ∈ ℂ)
99	98	subidd 11585	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → (𝑀 − 𝑀) = 0)
100	97, 99	eqtrd 2797	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → ((𝑌‘2) − (𝑋‘2)) = 0)
101	100	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = (0 · (𝑝‘1)))
102	3, 3, 9, 77	mp3an12i 1494	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 1⟩, ⟨2, 𝑀⟩}‘1) = 1)
103	75, 102	eqtrid 2809	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑌‘1) = 1)
104	96, 103	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = (𝑀 · 1))
105		ax-1rid 11198	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑀 · 1) = 𝑀)
106	104, 105	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘2) · (𝑌‘1)) = 𝑀)
107	3, 6, 9, 82	mp3an12i 1494	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
108	80, 107	eqtrid 2809	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℝ → (𝑋‘1) = 0)
109	108, 92	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = (0 · 𝑀))
110	98	mul02d 11436	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (0 · 𝑀) = 0)
111	109, 110	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℝ → ((𝑋‘1) · (𝑌‘2)) = 0)
112	106, 111	oveq12d 7435	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (𝑀 − 0))
113	98	subid1d 11586	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (𝑀 − 0) = 𝑀)
114	112, 113	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = 𝑀)
115	101, 114	oveq12d 7435	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) = ((0 · (𝑝‘1)) + 𝑀))
116	88, 115	eqeq12d 2778	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
117	116	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀)))
118	19, 28	rrx2pyel 49650	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ)
119	118	recnd 11265	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ)
120	119	mullidd 11255	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → (1 · (𝑝‘2)) = (𝑝‘2))
121	19, 28	rrx2pxel 49649	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
122	121	recnd 11265	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
123	122	mul02d 11436	. . . . . . . . 9 ⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘1)) = 0)
124	123	oveq1d 7432	. . . . . . . 8 ⊢ (𝑝 ∈ 𝑃 → ((0 · (𝑝‘1)) + 𝑀) = (0 + 𝑀))
125	120, 124	eqeq12d 2778	. . . . . . 7 ⊢ (𝑝 ∈ 𝑃 → ((1 · (𝑝‘2)) = ((0 · (𝑝‘1)) + 𝑀) ↔ (𝑝‘2) = (0 + 𝑀)))
126	117, 125	sylan9bb 519	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ (𝑝‘2) = (0 + 𝑀)))
127	126	bibi2d 345	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
128	127	ralbidva 3185	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀))))
129	98	addlidd 11439	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → (0 + 𝑀) = 𝑀)
130	129	adantr 486	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → (0 + 𝑀) = 𝑀)
131	130	eqeq2d 2773	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (0 + 𝑀) ↔ (𝑝‘2) = 𝑀))
132	131	bibi2d 345	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
133	132	ralbidva 3185	. . . . 5 ⊢ (𝑀 ∈ ℝ → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
134	133	adantl 487	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (0 + 𝑀)) ↔ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀)))
135	19, 66, 28, 67, 1, 27, 43	line2xlem 49691	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀) → (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))))
136		oveq1 7424	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
137	136	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
138	137	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = (0 · (𝑝‘1)))
139	123	adantl 487	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 · (𝑝‘1)) = 0)
140	138, 139	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = 0)
141	140	oveq1d 7432	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (0 + (𝐵 · (𝑝‘2))))
142		recn 11218	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
143	142	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
144	143	3ad2ant2 1152	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
145	144	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
146	119	adantl 487	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℂ)
147	145, 146	mulcld 11257	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ)
148	147	addlidd 11439	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (0 + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
149	141, 148	eqtrd 2797	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = (𝐵 · (𝑝‘2)))
150	149	eqeq1d 2764	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝐵 · (𝑝‘2)) = 𝐶))
151		simp3 1156	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
152	151	recnd 11265	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
153	152	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ)
154		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℝ)
155	154	recnd 11265	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
156	155	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
157	156	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
158		simp2r 1219	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ≠ 0)
159	158	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → 𝐵 ≠ 0)
160	153, 157, 146, 159	divmuld 12041	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ (𝐵 · (𝑝‘2)) = 𝐶))
161		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → 𝑀 = (𝐶 / 𝐵))
162	161	eqcomd 2768	. . . . . . . . . . 11 ⊢ ((𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵)) → (𝐶 / 𝐵) = 𝑀)
163	162	ad2antlr 740	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) = 𝑀)
164	163	eqeq1d 2764	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) = (𝑝‘2) ↔ 𝑀 = (𝑝‘2)))
165	150, 160, 164	3bitr2d 310	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ 𝑀 = (𝑝‘2)))
166		eqcom 2769	. . . . . . . 8 ⊢ (𝑀 = (𝑝‘2) ↔ (𝑝‘2) = 𝑀)
167	165, 166	bitrdi 290	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
168	167	ralrimiva 3156	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑀 ∈ ℝ) ∧ (𝐴 = 0 ∧ 𝑀 = (𝐶 / 𝐵))) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = 𝑀))
169	168	ex 418	. . . . 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

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 {crab 3414 Vcvv 3453 ⊆ wss 3902 {cpr 4589 ⟨cop 4593 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ↑_m cmap 8830 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 · cmul 11133 − cmin 11469 / cdiv 11899 2c2 12323 ℝ^crrx 25617 Line_Mcline 49665

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206 ax-addf 11207 ax-mulf 11208

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-sup 9416 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-z 12620 df-dec 12741 df-uz 12892 df-rp 13047 df-fz 13566 df-seq 14070 df-exp 14130 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-starv 17363 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-unif 17371 df-hom 17372 df-cco 17373 df-0g 17532 df-prds 17538 df-pws 17540 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-grp 19066 df-minusg 19067 df-sbg 19068 df-subg 19252 df-ghm 19347 df-cmn 19915 df-abl 19916 df-mgp 20280 df-rng 20294 df-ur 20327 df-ring 20380 df-cring 20381 df-oppr 20484 df-dvdsr 20504 df-unit 20505 df-invr 20535 df-dvr 20548 df-rhm 20619 df-subrng 20714 df-subrg 20738 df-drng 20898 df-field 20899 df-staf 21011 df-srng 21012 df-lmod 21052 df-lss 21122 df-sra 21363 df-rgmod 21364 df-cnfld 21592 df-refld 21824 df-dsmm 21951 df-frlm 21966 df-tng 24816 df-tcph 25403 df-rrx 25619 df-line 49667

This theorem is used by: (None)

W3C validator