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 49576

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 11221	. . . . . . . . . . . 12 ⊢ 1 ∈ V
4		2ex 12336	. . . . . . . . . . . 12 ⊢ 2 ∈ V
5	3, 4	pm3.2i 476	. . . . . . . . . . 11 ⊢ (1 ∈ V ∧ 2 ∈ V)
6		c0ex 11218	. . . . . . . . . . . 12 ⊢ 0 ∈ V
7	6	jctl 533	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → (0 ∈ V ∧ 𝑀 ∈ ℝ))
8		1ne2 12469	. . . . . . . . . . . 12 ⊢ 1 ≠ 2
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ → 1 ≠ 2)
10		fprg 7159	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶{0, 𝑀})
11		0red 11229	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → 0 ∈ ℝ)
12		simp2r 1219	. . . . . . . . . . . . 13 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → 𝑀 ∈ ℝ)
13	11, 12	prssd 4793	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0, 𝑀} ⊆ ℝ)
14	10, 13	fssd 6730	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
15	5, 7, 9, 14	mp3an2i 1495	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
16		line2.i	. . . . . . . . . . 11 ⊢ 𝐼 = {1, 2}
17	16	feq2i 6704	. . . . . . . . . 10 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:{1, 2}⟶ℝ)
18	15, 17	sylibr 237	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
19		reex 11209	. . . . . . . . . 10 ⊢ ℝ ∈ V
20		prex 5414	. . . . . . . . . . 11 ⊢ {1, 2} ∈ V
21	16, 20	eqeltri 2862	. . . . . . . . . 10 ⊢ 𝐼 ∈ V
22	19, 21	elmap 8878	. . . . . . . . 9 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑀⟩}:𝐼⟶ℝ)
23	18, 22	sylibr 237	. . . . . . . 8 ⊢ (𝑀 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑀⟩} ∈ (ℝ ↑_m 𝐼))
24		line2y.x	. . . . . . . 8 ⊢ 𝑋 = {⟨1, 0⟩, ⟨2, 𝑀⟩}
25		line2.p	. . . . . . . 8 ⊢ 𝑃 = (ℝ ↑_m 𝐼)
26	23, 24, 25	3eltr4g 2883	. . . . . . 7 ⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃)
27	26	3ad2ant1 1151	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑋 ∈ 𝑃)
28	6	jctl 533	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → (0 ∈ V ∧ 𝑁 ∈ ℝ))
29	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → 1 ≠ 2)
30		fprg 7159	. . . . . . . . . . . 12 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑁 ∈ ℝ) ∧ 1 ≠ 2) → {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶{0, 𝑁})
31	5, 28, 29, 30	mp3an2i 1495	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶{0, 𝑁})
32		0re 11228	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
33		prssi 4792	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → {0, 𝑁} ⊆ ℝ)
34	32, 33	mpan 703	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → {0, 𝑁} ⊆ ℝ)
35	31, 34	fssd 6730	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶ℝ)
36	16	feq2i 6704	. . . . . . . . . 10 ⊢ ({⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ ↔ {⟨1, 0⟩, ⟨2, 𝑁⟩}:{1, 2}⟶ℝ)
37	35, 36	sylibr 237	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ)
38	19, 21	pm3.2i 476	. . . . . . . . . 10 ⊢ (ℝ ∈ V ∧ 𝐼 ∈ V)
39		elmapg 8845	. . . . . . . . . 10 ⊢ ((ℝ ∈ V ∧ 𝐼 ∈ V) → ({⟨1, 0⟩, ⟨2, 𝑁⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ))
40	38, 39	mp1i 14	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → ({⟨1, 0⟩, ⟨2, 𝑁⟩} ∈ (ℝ ↑_m 𝐼) ↔ {⟨1, 0⟩, ⟨2, 𝑁⟩}:𝐼⟶ℝ))
41	37, 40	mpbird 260	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → {⟨1, 0⟩, ⟨2, 𝑁⟩} ∈ (ℝ ↑_m 𝐼))
42		line2y.y	. . . . . . . 8 ⊢ 𝑌 = {⟨1, 0⟩, ⟨2, 𝑁⟩}
43	41, 42, 25	3eltr4g 2883	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → 𝑌 ∈ 𝑃)
44	43	3ad2ant2 1152	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑌 ∈ 𝑃)
45	24	fveq1i 6889	. . . . . . . . 9 ⊢ (𝑋‘1) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1)
46	3, 6, 8	3pm3.2i 1358	. . . . . . . . . 10 ⊢ (1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2)
47		fvpr1g 7195	. . . . . . . . . 10 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
48	46, 47	mp1i 14	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0)
49	45, 48	eqtrid 2813	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘1) = 0)
50	42	fveq1i 6889	. . . . . . . . 9 ⊢ (𝑌‘1) = ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘1)
51		fvpr1g 7195	. . . . . . . . . 10 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘1) = 0)
52	46, 51	mp1i 14	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘1) = 0)
53	50, 52	eqtrid 2813	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑌‘1) = 0)
54	49, 53	eqtr4d 2804	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘1) = (𝑌‘1))
55		simp3 1156	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑀 ≠ 𝑁)
56	24	fveq1i 6889	. . . . . . . . 9 ⊢ (𝑋‘2) = ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2)
57		simp1 1154	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ ℝ)
58	8	a1i 11	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 1 ≠ 2)
59		fvpr2g 7196	. . . . . . . . . 10 ⊢ ((2 ∈ V ∧ 𝑀 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
60	4, 57, 58, 59	mp3an2i 1495	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘2) = 𝑀)
61	56, 60	eqtrid 2813	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘2) = 𝑀)
62	42	fveq1i 6889	. . . . . . . . 9 ⊢ (𝑌‘2) = ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘2)
63		simp2 1155	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑁 ∈ ℝ)
64		fvpr2g 7196	. . . . . . . . . 10 ⊢ ((2 ∈ V ∧ 𝑁 ∈ ℝ ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘2) = 𝑁)
65	4, 63, 58, 64	mp3an2i 1495	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({⟨1, 0⟩, ⟨2, 𝑁⟩}‘2) = 𝑁)
66	62, 65	eqtrid 2813	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑌‘2) = 𝑁)
67	55, 61, 66	3netr4d 3038	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘2) ≠ (𝑌‘2))
68	54, 67	jca 521	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2)))
69	27, 44, 68	3jca 1146	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))))
70	69	adantl 487	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))))
71		line2.e	. . . . 5 ⊢ 𝐸 = (ℝ^‘𝐼)
72		line2.l	. . . . 5 ⊢ 𝐿 = (Line_M‘𝐸)
73	16, 71, 25, 72	rrx2vlinest 49562	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)})
74	70, 73	syl 18	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)})
75	2, 74	eqeq12d 2782	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)}))
76	46, 47	ax-mp 5	. . . . . . 7 ⊢ ({⟨1, 0⟩, ⟨2, 𝑀⟩}‘1) = 0
77	45, 76	eqtri 2789	. . . . . 6 ⊢ (𝑋‘1) = 0
78	77	a1i 11	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋‘1) = 0)
79	78	eqeq2d 2777	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ((𝑝‘1) = (𝑋‘1) ↔ (𝑝‘1) = 0))
80	79	rabbidv 3426	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0})
81	80	eqeq2d 2777	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)} ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0}))
82		rabbi 3449	. . 3 ⊢ (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0})
83	16, 25	line2ylem 49572	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
84	83	adantr 486	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
85		oveq1 7430	. . . . . . . . . . 11 ⊢ (𝐵 = 0 → (𝐵 · (𝑝‘2)) = (0 · (𝑝‘2)))
86	85	3ad2ant2 1152	. . . . . . . . . 10 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (𝐵 · (𝑝‘2)) = (0 · (𝑝‘2)))
87	86	oveq2d 7439	. . . . . . . . 9 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))))
88		simp3 1156	. . . . . . . . 9 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → 𝐶 = 0)
89	87, 88	eqeq12d 2782	. . . . . . . 8 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0))
90	89	ad2antlr 740	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0))
91	16, 25	rrx2pyel 49533	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ)
92	91	recnd 11255	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ)
93	92	mul02d 11426	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘2)) = 0)
94	93	adantl 487	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (0 · (𝑝‘2)) = 0)
95	94	oveq2d 7439	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = ((𝐴 · (𝑝‘1)) + 0))
96		simp1 1154	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
97	96	recnd 11255	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
98	97	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℂ)
99	16, 25	rrx2pxel 49532	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
100	99	recnd 11255	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
101	100	adantl 487	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ)
102	98, 101	mulcld 11247	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℂ)
103	102	addridd 11428	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + 0) = (𝐴 · (𝑝‘1)))
104	95, 103	eqtrd 2801	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = (𝐴 · (𝑝‘1)))
105	104	eqeq1d 2768	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0 ↔ (𝐴 · (𝑝‘1)) = 0))
106	98, 101	mul0ord 11880	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) = 0 ↔ (𝐴 = 0 ∨ (𝑝‘1) = 0)))
107		eqneqall 2972	. . . . . . . . . . . . 13 ⊢ (𝐴 = 0 → (𝐴 ≠ 0 → (𝑝‘1) = 0))
108	107	com12 33	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 0 → (𝐴 = 0 → (𝑝‘1) = 0))
109	108	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (𝐴 = 0 → (𝑝‘1) = 0))
110	109	ad2antlr 740	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝐴 = 0 → (𝑝‘1) = 0))
111		idd 25	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = 0 → (𝑝‘1) = 0))
112	110, 111	jaod 873	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 = 0 ∨ (𝑝‘1) = 0) → (𝑝‘1) = 0))
113		olc 882	. . . . . . . . 9 ⊢ ((𝑝‘1) = 0 → (𝐴 = 0 ∨ (𝑝‘1) = 0))
114	112, 113	impbid1 228	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 = 0 ∨ (𝑝‘1) = 0) ↔ (𝑝‘1) = 0))
115	106, 114	bitrd 282	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) = 0 ↔ (𝑝‘1) = 0))
116	90, 105, 115	3bitrd 308	. . . . . 6 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
117	116	ralrimiva 3160	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
118	117	ex 418	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
119	84, 118	impbid 215	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
120	82, 119	bitr3id 288	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0} ↔ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))
121	75, 81, 120	3bitrd 308	1 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝐺 = (𝑋𝐿𝑌) ↔ (𝐴 ≠ 0 ∧ 𝐵 = 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 2146 ≠ wne 2961 ∀wral 3082 {crab 3419 Vcvv 3458 ⊆ wss 3908 {cpr 4596 ⟨cop 4600 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 ↑_m cmap 8833 ℂcc 11116 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 · cmul 11123 2c2 12313 ℝ^crrx 25579 Line_Mcline 49548

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196 ax-addf 11197 ax-mulf 11198

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-of 7687 df-om 7872 df-1st 7995 df-2nd 7996 df-supp 8166 df-tpos 8231 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-er 8703 df-map 8835 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fsupp 9332 df-sup 9412 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12523 df-z 12610 df-dec 12730 df-uz 12881 df-rp 13035 df-fz 13554 df-seq 14058 df-exp 14118 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-struct 17232 df-sets 17249 df-slot 17267 df-ndx 17279 df-base 17295 df-ress 17316 df-plusg 17348 df-mulr 17349 df-starv 17350 df-sca 17351 df-vsca 17352 df-ip 17353 df-tset 17354 df-ple 17355 df-ds 17357 df-unif 17358 df-hom 17359 df-cco 17360 df-0g 17519 df-prds 17525 df-pws 17527 df-mgm 18723 df-sgrp 18806 df-mnd 18822 df-mhm 18872 df-grp 19034 df-minusg 19035 df-sbg 19036 df-subg 19220 df-ghm 19315 df-cmn 19883 df-abl 19884 df-mgp 20248 df-rng 20262 df-ur 20295 df-ring 20348 df-cring 20349 df-oppr 20452 df-dvdsr 20472 df-unit 20473 df-invr 20503 df-dvr 20516 df-rhm 20587 df-subrng 20682 df-subrg 20706 df-drng 20866 df-field 20867 df-staf 20979 df-srng 20980 df-lmod 21020 df-lss 21090 df-sra 21331 df-rgmod 21332 df-cnfld 21560 df-refld 21792 df-dsmm 21919 df-frlm 21934 df-tng 24778 df-tcph 25365 df-rrx 25581 df-line 49550

This theorem is used by: (None)

W3C validator