Proof of Theorem line2y
Step | Hyp | Ref
| Expression |
1 | | line2.g |
. . . 4
⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} |
2 | 1 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) |
3 | | 1ex 10981 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
4 | | 2ex 12060 |
. . . . . . . . . . . 12
⊢ 2 ∈
V |
5 | 3, 4 | pm3.2i 471 |
. . . . . . . . . . 11
⊢ (1 ∈
V ∧ 2 ∈ V) |
6 | | c0ex 10979 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
7 | 6 | jctl 524 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ → (0 ∈
V ∧ 𝑀 ∈
ℝ)) |
8 | | 1ne2 12191 |
. . . . . . . . . . . 12
⊢ 1 ≠
2 |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ → 1 ≠
2) |
10 | | fprg 7019 |
. . . . . . . . . . . 12
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) →
{〈1, 0〉, 〈2, 𝑀〉}:{1, 2}⟶{0, 𝑀}) |
11 | | 0red 10988 |
. . . . . . . . . . . . 13
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → 0
∈ ℝ) |
12 | | simp2r 1199 |
. . . . . . . . . . . . 13
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) →
𝑀 ∈
ℝ) |
13 | 11, 12 | prssd 4755 |
. . . . . . . . . . . 12
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) → {0,
𝑀} ⊆
ℝ) |
14 | 10, 13 | fssd 6610 |
. . . . . . . . . . 11
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑀 ∈ ℝ) ∧ 1 ≠ 2) →
{〈1, 0〉, 〈2, 𝑀〉}:{1,
2}⟶ℝ) |
15 | 5, 7, 9, 14 | mp3an2i 1465 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℝ → {〈1,
0〉, 〈2, 𝑀〉}:{1,
2}⟶ℝ) |
16 | | line2.i |
. . . . . . . . . . 11
⊢ 𝐼 = {1, 2} |
17 | 16 | feq2i 6584 |
. . . . . . . . . 10
⊢
({〈1, 0〉, 〈2, 𝑀〉}:𝐼⟶ℝ ↔ {〈1, 0〉,
〈2, 𝑀〉}:{1,
2}⟶ℝ) |
18 | 15, 17 | sylibr 233 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℝ → {〈1,
0〉, 〈2, 𝑀〉}:𝐼⟶ℝ) |
19 | | reex 10972 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
20 | | prex 5353 |
. . . . . . . . . . 11
⊢ {1, 2}
∈ V |
21 | 16, 20 | eqeltri 2835 |
. . . . . . . . . 10
⊢ 𝐼 ∈ V |
22 | 19, 21 | elmap 8646 |
. . . . . . . . 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 2856 |
. . . . . . 7
⊢ (𝑀 ∈ ℝ → 𝑋 ∈ 𝑃) |
27 | 26 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑋 ∈ 𝑃) |
28 | 6 | jctl 524 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → (0 ∈
V ∧ 𝑁 ∈
ℝ)) |
29 | 8 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → 1 ≠
2) |
30 | | fprg 7019 |
. . . . . . . . . . . 12
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ 𝑁 ∈ ℝ) ∧ 1 ≠ 2) →
{〈1, 0〉, 〈2, 𝑁〉}:{1, 2}⟶{0, 𝑁}) |
31 | 5, 28, 29, 30 | mp3an2i 1465 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → {〈1,
0〉, 〈2, 𝑁〉}:{1, 2}⟶{0, 𝑁}) |
32 | | 0re 10987 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
33 | | prssi 4754 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ) → {0, 𝑁} ⊆ ℝ) |
34 | 32, 33 | mpan 687 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → {0, 𝑁} ⊆
ℝ) |
35 | 31, 34 | fssd 6610 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → {〈1,
0〉, 〈2, 𝑁〉}:{1,
2}⟶ℝ) |
36 | 16 | feq2i 6584 |
. . . . . . . . . 10
⊢
({〈1, 0〉, 〈2, 𝑁〉}:𝐼⟶ℝ ↔ {〈1, 0〉,
〈2, 𝑁〉}:{1,
2}⟶ℝ) |
37 | 35, 36 | sylibr 233 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℝ → {〈1,
0〉, 〈2, 𝑁〉}:𝐼⟶ℝ) |
38 | 19, 21 | pm3.2i 471 |
. . . . . . . . . 10
⊢ (ℝ
∈ V ∧ 𝐼 ∈
V) |
39 | | elmapg 8615 |
. . . . . . . . . 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 256 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ → {〈1,
0〉, 〈2, 𝑁〉}
∈ (ℝ ↑m 𝐼)) |
42 | | line2y.y |
. . . . . . . 8
⊢ 𝑌 = {〈1, 0〉, 〈2,
𝑁〉} |
43 | 41, 42, 25 | 3eltr4g 2856 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ → 𝑌 ∈ 𝑃) |
44 | 43 | 3ad2ant2 1133 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑌 ∈ 𝑃) |
45 | 24 | fveq1i 6767 |
. . . . . . . . 9
⊢ (𝑋‘1) = ({〈1, 0〉,
〈2, 𝑀〉}‘1) |
46 | 3, 6, 8 | 3pm3.2i 1338 |
. . . . . . . . . 10
⊢ (1 ∈
V ∧ 0 ∈ V ∧ 1 ≠ 2) |
47 | | fvpr1g 7054 |
. . . . . . . . . 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 2790 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘1) = 0) |
50 | 42 | fveq1i 6767 |
. . . . . . . . 9
⊢ (𝑌‘1) = ({〈1, 0〉,
〈2, 𝑁〉}‘1) |
51 | | fvpr1g 7054 |
. . . . . . . . . 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 2790 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑌‘1) = 0) |
54 | 49, 53 | eqtr4d 2781 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘1) = (𝑌‘1)) |
55 | | simp3 1137 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑀 ≠ 𝑁) |
56 | 24 | fveq1i 6767 |
. . . . . . . . 9
⊢ (𝑋‘2) = ({〈1, 0〉,
〈2, 𝑀〉}‘2) |
57 | | simp1 1135 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ ℝ) |
58 | 8 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 1 ≠ 2) |
59 | | fvpr2g 7055 |
. . . . . . . . . 10
⊢ ((2
∈ V ∧ 𝑀 ∈
ℝ ∧ 1 ≠ 2) → ({〈1, 0〉, 〈2, 𝑀〉}‘2) = 𝑀) |
60 | 4, 57, 58, 59 | mp3an2i 1465 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({〈1, 0〉, 〈2, 𝑀〉}‘2) = 𝑀) |
61 | 56, 60 | eqtrid 2790 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘2) = 𝑀) |
62 | 42 | fveq1i 6767 |
. . . . . . . . 9
⊢ (𝑌‘2) = ({〈1, 0〉,
〈2, 𝑁〉}‘2) |
63 | | simp2 1136 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → 𝑁 ∈ ℝ) |
64 | | fvpr2g 7055 |
. . . . . . . . . 10
⊢ ((2
∈ V ∧ 𝑁 ∈
ℝ ∧ 1 ≠ 2) → ({〈1, 0〉, 〈2, 𝑁〉}‘2) = 𝑁) |
65 | 4, 63, 58, 64 | mp3an2i 1465 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ({〈1, 0〉, 〈2, 𝑁〉}‘2) = 𝑁) |
66 | 62, 65 | eqtrid 2790 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑌‘2) = 𝑁) |
67 | 55, 61, 66 | 3netr4d 3021 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋‘2) ≠ (𝑌‘2)) |
68 | 54, 67 | jca 512 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))) |
69 | 27, 44, 68 | 3jca 1127 |
. . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2)))) |
70 | 69 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2)))) |
71 | | line2.e |
. . . . 5
⊢ 𝐸 = (ℝ^‘𝐼) |
72 | | line2.l |
. . . . 5
⊢ 𝐿 = (LineM‘𝐸) |
73 | 16, 71, 25, 72 | rrx2vlinest 46065 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) ≠ (𝑌‘2))) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)}) |
74 | 70, 73 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)}) |
75 | 2, 74 | eqeq12d 2754 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝐺 = (𝑋𝐿𝑌) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)})) |
76 | 46, 47 | ax-mp 5 |
. . . . . . 7
⊢
({〈1, 0〉, 〈2, 𝑀〉}‘1) = 0 |
77 | 45, 76 | eqtri 2766 |
. . . . . 6
⊢ (𝑋‘1) = 0 |
78 | 77 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (𝑋‘1) = 0) |
79 | 78 | eqeq2d 2749 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ((𝑝‘1) = (𝑋‘1) ↔ (𝑝‘1) = 0)) |
80 | 79 | rabbidv 3411 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0}) |
81 | 80 | eqeq2d 2749 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → ({𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (𝑋‘1)} ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0})) |
82 | | rabbi 3314 |
. . 3
⊢
(∀𝑝 ∈
𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = 0}) |
83 | 16, 25 | line2ylem 46075 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
(∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0))) |
84 | 83 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0))) |
85 | | oveq1 7274 |
. . . . . . . . . . 11
⊢ (𝐵 = 0 → (𝐵 · (𝑝‘2)) = (0 · (𝑝‘2))) |
86 | 85 | 3ad2ant2 1133 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (𝐵 · (𝑝‘2)) = (0 · (𝑝‘2))) |
87 | 86 | oveq2d 7283 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2)))) |
88 | | simp3 1137 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → 𝐶 = 0) |
89 | 87, 88 | eqeq12d 2754 |
. . . . . . . 8
⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0)) |
90 | 89 | ad2antlr 724 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0)) |
91 | 16, 25 | rrx2pyel 46036 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ) |
92 | 91 | recnd 11013 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ) |
93 | 92 | mul02d 11183 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ 𝑃 → (0 · (𝑝‘2)) = 0) |
94 | 93 | adantl 482 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (0 · (𝑝‘2)) = 0) |
95 | 94 | oveq2d 7283 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = ((𝐴 · (𝑝‘1)) + 0)) |
96 | | simp1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈
ℝ) |
97 | 96 | recnd 11013 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈
ℂ) |
98 | 97 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℂ) |
99 | 16, 25 | rrx2pxel 46035 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ) |
100 | 99 | recnd 11013 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ) |
101 | 100 | adantl 482 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ) |
102 | 98, 101 | mulcld 11005 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℂ) |
103 | 102 | addid1d 11185 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + 0) = (𝐴 · (𝑝‘1))) |
104 | 95, 103 | eqtrd 2778 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = (𝐴 · (𝑝‘1))) |
105 | 104 | eqeq1d 2740 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (0 · (𝑝‘2))) = 0 ↔ (𝐴 · (𝑝‘1)) = 0)) |
106 | 98, 101 | mul0ord 11635 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) = 0 ↔ (𝐴 = 0 ∨ (𝑝‘1) = 0))) |
107 | | eqneqall 2954 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 0 → (𝐴 ≠ 0 → (𝑝‘1) = 0)) |
108 | 107 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ 0 → (𝐴 = 0 → (𝑝‘1) = 0)) |
109 | 108 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) → (𝐴 = 0 → (𝑝‘1) = 0)) |
110 | 109 | ad2antlr 724 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → (𝐴 = 0 → (𝑝‘1) = 0)) |
111 | | idd 24 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = 0 → (𝑝‘1) = 0)) |
112 | 110, 111 | jaod 856 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 = 0 ∨ (𝑝‘1) = 0) → (𝑝‘1) = 0)) |
113 | | olc 865 |
. . . . . . . . 9
⊢ ((𝑝‘1) = 0 → (𝐴 = 0 ∨ (𝑝‘1) = 0)) |
114 | 112, 113 | impbid1 224 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ ∧ 𝐶 ∈
ℝ) ∧ (𝑀 ∈
ℝ ∧ 𝑁 ∈
ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 = 0 ∨ (𝑝‘1) = 0) ↔ (𝑝‘1) = 0)) |
115 | 106, 114 | bitrd 278 |
. . . . . . 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 3108 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≠ 𝑁)) ∧ (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)) → ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)) |
118 | 117 | ex 413 |
. . . 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))) |