line2y - Mathbox for Alexander van der Vekens

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

Theorem line2y 47395

Description: Example for a vertical 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))) = 𝐶}
line2y.x	⊢ 𝑋 = {⟨1, 0⟩, ⟨2, 𝑀⟩}
line2y.y	⊢ 𝑌 = {⟨1, 0⟩, ⟨2, 𝑁⟩}

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

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

**Proof of Theorem line2y**
Step	Hyp	Ref	Expression
1		line2.g	. . . 4 ⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}
2	1	a1i 11	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶})
3		1ex 11207	. . . . . . . . . . . 12 ⊢ 1 ∈ V
4		2ex 12286	. . . . . . . . . . . 12 ⊢ 2 ∈ V
5	3, 4	pm3.2i 472	. . . . . . . . . . 11 ⊢ (1 ∈ V ∧ 2 ∈ V)
6		c0ex 11205	. . . . . . . . . . . 12 ⊢ 0 ∈ V
7	6	jctl 525	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (0 ∈ V ∧ 𝑀 ∈ ℝ))
8		1ne2 12417	. . . . . . . . . . . 12 ⊢ 1 ≠ 2
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → 1 ≠ 2)
10		fprg 7150	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{0, 𝑀})
11		0red 11214	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → 0 ∈ ℝ)
12		simp2r 1201	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → 𝑀 ∈ ℝ)
13	11, 12	prssd 4825	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0, 𝑀} ⊆ ℝ)
14	10, 13	fssd 6733	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
15	5, 7, 9, 14	mp3an2i 1467	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
16		line2.i	. . . . . . . . . . 11 ⊢ 𝐼 = {1, 2}
17	16	feq2i 6707	. . . . . . . . . 10 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
18	15, 17	sylibr 233	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
19		reex 11198	. . . . . . . . . 10 ⊢ ℝ ∈ V
20		prex 5432	. . . . . . . . . . 11 ⊢ {1, 2} ∈ V
21	16, 20	eqeltri 2830	. . . . . . . . . 10 ⊢ 𝐼 ∈ V
22	19, 21	elmap 8862	. . . . . . . . 9 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
23	18, 22	sylibr 233	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼))
24		line2y.x	. . . . . . . 8 ⊢ 𝑋 = {⟨1, 0⟩, ⟨2, 𝑀⟩}
25		line2.p	. . . . . . . 8 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
26	23, 24, 25	3eltr4g 2851	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃)
27	26	3ad2ant1 1134	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑋 ∈ 𝑃)
28	6	jctl 525	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → (0 ∈ V ∧ 𝑁 ∈ ℝ))
29	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → 1 ≠ 2)
30		fprg 7150	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑁 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶{0, 𝑁})
31	5, 28, 29, 30	mp3an2i 1467	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶{0, 𝑁})
32		0re 11213	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
33		prssi 4824	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → {0, 𝑁} ⊆ ℝ)
34	32, 33	mpan 689	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → {0, 𝑁} ⊆ ℝ)
35	31, 34	fssd 6733	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶ℝ)
36	16	feq2i 6707	. . . . . . . . . 10 ⊢ ({⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶ℝ)
37	35, 36	sylibr 233	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ)
38	19, 21	pm3.2i 472	. . . . . . . . . 10 ⊢ (ℝ ∈ V ∧ 𝐼 ∈ V)
39		elmapg 8830	. . . . . . . . . 10 ⊢ ((ℝ ∈ V ∧ 𝐼 ∈ V) → ({⟨1, 0⟩, ⟨2, 𝑁⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ))
40	38, 39	mp1i 13	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑁⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ))
41	37, 40	mpbird 257	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩} ∈ (ℝ ↑_m 𝐼))
42		line2y.y	. . . . . . . 8 ⊢ 𝑌 = {⟨1, 0⟩, ⟨2, 𝑁⟩}
43	41, 42, 25	3eltr4g 2851	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → 𝑌 ∈ 𝑃)
44	43	3ad2ant2 1135	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑌 ∈ 𝑃)
45	24	fveq1i 6890	. . . . . . . . 9 ⊢ (𝑋‘1) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1)
46	3, 6, 8	3pm3.2i 1340	. . . . . . . . . 10 ⊢ (1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2)
47		fvpr1g 7185	. . . . . . . . . 10 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
48	46, 47	mp1i 13	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
49	45, 48	eqtrid 2785	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘1) = 0)
50	42	fveq1i 6890	. . . . . . . . 9 ⊢ (𝑌‘1) = ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘1)
51		fvpr1g 7185	. . . . . . . . . 10 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘1) = 0)
52	46, 51	mp1i 13	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘1) = 0)
53	50, 52	eqtrid 2785	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑌‘1) = 0)
54	49, 53	eqtr4d 2776	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘1) = (𝑌‘1))
55		simp3 1139	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑀 ≠ 𝑁)
56	24	fveq1i 6890	. . . . . . . . 9 ⊢ (𝑋‘2) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2)
57		simp1 1137	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ ℝ)
58	8	a1i 11	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 1 ≠ 2)
59		fvpr2g 7186	. . . . . . . . . 10 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
60	4, 57, 58, 59	mp3an2i 1467	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
61	56, 60	eqtrid 2785	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘2) = 𝑀)
62	42	fveq1i 6890	. . . . . . . . 9 ⊢ (𝑌‘2) = ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘2)
63		simp2 1138	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑁 ∈ ℝ)
64		fvpr2g 7186	. . . . . . . . . 10 ⊢ ((2 ∈ V ∧ 𝑁 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘2) = 𝑁)
65	4, 63, 58, 64	mp3an2i 1467	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘2) = 𝑁)
66	62, 65	eqtrid 2785	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑌‘2) = 𝑁)
67	55, 61, 66	3netr4d 3019	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘2) ≠ (𝑌‘2))
68	54, 67	jca 513	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2)))
69	27, 44, 68	3jca 1129	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))))
70	69	adantl 483	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))))
71		line2.e	. . . . 5 ⊢ 𝐸 = (ℝ^‘𝐼)
72		line2.l	. . . . 5 ⊢ 𝐿 = (Line_M‘𝐸)
73	16, 71, 25, 72	rrx2vlinest 47381	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)})
74	70, 73	syl 17	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)})
75	2, 74	eqeq12d 2749	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)}))
76	46, 47	ax-mp 5	. . . . . . 7 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0
77	45, 76	eqtri 2761	. . . . . 6 ⊢ (𝑋‘1) = 0
78	77	a1i 11	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋‘1) = 0)
79	78	eqeq2d 2744	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ((𝑝‘1) = (𝑋‘1) ↔ (𝑝‘1) = 0))
80	79	rabbidv 3441	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0})
81	80	eqeq2d 2744	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)} ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0}))
82		rabbi 3463	. . 3 ⊢ (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0})
83	16, 25	line2ylem 47391	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
84	83	adantr 482	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
85		oveq1 7413	. . . . . . . . . . 11 ⊢ (𝐵 = 0 → (𝐵 · (𝑝‘2)) = (0 · (𝑝‘2)))
86	85	3ad2ant2 1135	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (𝐵 · (𝑝‘2)) = (0 · (𝑝‘2)))
87	86	oveq2d 7422	. . . . . . . . 9 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))))
88		simp3 1139	. . . . . . . . 9 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → 𝐶 = 0)
89	87, 88	eqeq12d 2749	. . . . . . . 8 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0))
90	89	ad2antlr 726	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0))
91	16, 25	rrx2pyel 47352	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ)
92	91	recnd 11239	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ)
93	92	mul02d 11409	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘2)) = 0)
94	93	adantl 483	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (0 · (𝑝‘2)) = 0)
95	94	oveq2d 7422	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = ((𝐴 · (𝑝‘1)) + 0))
96		simp1 1137	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
97	96	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
98	97	ad3antrrr 729	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℂ)
99	16, 25	rrx2pxel 47351	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
100	99	recnd 11239	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
101	100	adantl 483	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ)
102	98, 101	mulcld 11231	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℂ)
103	102	addridd 11411	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + 0) = (𝐴 · (𝑝‘1)))
104	95, 103	eqtrd 2773	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = (𝐴 · (𝑝‘1)))
105	104	eqeq1d 2735	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0 ↔ (𝐴 · (𝑝‘1)) = 0))
106	98, 101	mul0ord 11861	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) = 0 ↔ (𝐴 = 0 ∨ (𝑝‘1) = 0)))
107		eqneqall 2952	. . . . . . . . . . . . 13 ⊢ (𝐴 = 0 → (𝐴 ≠ 0 → (𝑝‘1) = 0))
108	107	com12 32	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 0 → (𝐴 = 0 → (𝑝‘1) = 0))
109	108	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (𝐴 = 0 → (𝑝‘1) = 0))
110	109	ad2antlr 726	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝐴 = 0 → (𝑝‘1) = 0))
111		idd 24	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = 0 → (𝑝‘1) = 0))
112	110, 111	jaod 858	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 = 0 ∨ (𝑝‘1) = 0) → (𝑝‘1) = 0))
113		olc 867	. . . . . . . . 9 ⊢ ((𝑝‘1) = 0 → (𝐴 = 0 ∨ (𝑝‘1) = 0))
114	112, 113	impbid1 224	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 = 0 ∨ (𝑝‘1) = 0) ↔ (𝑝‘1) = 0))
115	106, 114	bitrd 279	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) = 0 ↔ (𝑝‘1) = 0))
116	90, 105, 115	3bitrd 305	. . . . . 6 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
117	116	ralrimiva 3147	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
118	117	ex 414	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
119	84, 118	impbid 211	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
120	82, 119	bitr3id 285	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0} ↔ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
121	75, 81, 120	3bitrd 305	1 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 {crab 3433 Vcvv 3475 ⊆ wss 3948 {cpr 4630 ⟨cop 4634 ⟶wf 6537 ‘cfv 6541 (class class class)co 7406 ↑_m cmap 8817 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 · cmul 11112 2c2 12264 ℝ^crrx 24892 Line_Mcline 47367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-tpos 8208 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-er 8700 df-map 8819 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-sup 9434 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-rp 12972 df-fz 13482 df-seq 13964 df-exp 14025 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-0g 17384 df-prds 17390 df-pws 17392 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-mhm 18668 df-grp 18819 df-minusg 18820 df-sbg 18821 df-subg 18998 df-ghm 19085 df-cmn 19645 df-mgp 19983 df-ur 20000 df-ring 20052 df-cring 20053 df-oppr 20143 df-dvdsr 20164 df-unit 20165 df-invr 20195 df-dvr 20208 df-rnghom 20244 df-drng 20310 df-field 20311 df-subrg 20354 df-staf 20446 df-srng 20447 df-lmod 20466 df-lss 20536 df-sra 20778 df-rgmod 20779 df-cnfld 20938 df-refld 21150 df-dsmm 21279 df-frlm 21294 df-tng 24085 df-tcph 24678 df-rrx 24894 df-line 47369

This theorem is referenced by: (None)

W3C validator