Step | Hyp | Ref
| Expression |
1 | | mptscmfsupp0.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
2 | | mptexg 6389 |
. . 3
⊢ (𝐷 ∈ 𝑉 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) ∈ V) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) ∈ V) |
4 | | funmpt 5840 |
. . 3
⊢ Fun
(𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → Fun (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))) |
6 | | mptscmfsupp0.0 |
. . . 4
⊢ 0 =
(0g‘𝑄) |
7 | | fvex 6113 |
. . . 4
⊢
(0g‘𝑄) ∈ V |
8 | 6, 7 | eqeltri 2684 |
. . 3
⊢ 0 ∈
V |
9 | 8 | a1i 11 |
. 2
⊢ (𝜑 → 0 ∈ V) |
10 | | mptscmfsupp0.f |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ 𝑆) finSupp 𝑍) |
11 | 10 | fsuppimpd 8165 |
. 2
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) ∈ Fin) |
12 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑑 ∈ 𝐷) |
13 | | mptscmfsupp0.s |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑆 ∈ 𝐵) |
14 | 13 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ 𝐷 𝑆 ∈ 𝐵) |
15 | 14 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ∀𝑘 ∈ 𝐷 𝑆 ∈ 𝐵) |
16 | | rspcsbela 3958 |
. . . . . . . . 9
⊢ ((𝑑 ∈ 𝐷 ∧ ∀𝑘 ∈ 𝐷 𝑆 ∈ 𝐵) → ⦋𝑑 / 𝑘⦌𝑆 ∈ 𝐵) |
17 | 12, 15, 16 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌𝑆 ∈ 𝐵) |
18 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐷 ↦ 𝑆) = (𝑘 ∈ 𝐷 ↦ 𝑆) |
19 | 18 | fvmpts 6194 |
. . . . . . . 8
⊢ ((𝑑 ∈ 𝐷 ∧ ⦋𝑑 / 𝑘⦌𝑆 ∈ 𝐵) → ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = ⦋𝑑 / 𝑘⦌𝑆) |
20 | 12, 17, 19 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = ⦋𝑑 / 𝑘⦌𝑆) |
21 | 20 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = 𝑍 ↔ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍)) |
22 | | oveq1 6556 |
. . . . . . . . 9
⊢
(⦋𝑑 /
𝑘⦌𝑆 = 𝑍 → (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = (𝑍 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
23 | | mptscmfsupp0.z |
. . . . . . . . . . . 12
⊢ 𝑍 = (0g‘𝑅) |
24 | | mptscmfsupp0.r |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (Scalar‘𝑄)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑅 = (Scalar‘𝑄)) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (0g‘𝑅) =
(0g‘(Scalar‘𝑄))) |
27 | 23, 26 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑍 = (0g‘(Scalar‘𝑄))) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (𝑍 ∗
⦋𝑑 / 𝑘⦌𝑊) =
((0g‘(Scalar‘𝑄)) ∗
⦋𝑑 / 𝑘⦌𝑊)) |
29 | | mptscmfsupp0.q |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ LMod) |
30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑄 ∈ LMod) |
31 | | mptscmfsupp0.w |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑊 ∈ 𝐾) |
32 | 31 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝐷 𝑊 ∈ 𝐾) |
33 | 32 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ∀𝑘 ∈ 𝐷 𝑊 ∈ 𝐾) |
34 | | rspcsbela 3958 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝐷 ∧ ∀𝑘 ∈ 𝐷 𝑊 ∈ 𝐾) → ⦋𝑑 / 𝑘⦌𝑊 ∈ 𝐾) |
35 | 12, 33, 34 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌𝑊 ∈ 𝐾) |
36 | | mptscmfsupp0.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (Base‘𝑄) |
37 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
38 | | mptscmfsupp0.m |
. . . . . . . . . . . 12
⊢ ∗ = (
·𝑠 ‘𝑄) |
39 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝑄)) =
(0g‘(Scalar‘𝑄)) |
40 | 36, 37, 38, 39, 6 | lmod0vs 18719 |
. . . . . . . . . . 11
⊢ ((𝑄 ∈ LMod ∧
⦋𝑑 / 𝑘⦌𝑊 ∈ 𝐾) →
((0g‘(Scalar‘𝑄)) ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
41 | 30, 35, 40 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) →
((0g‘(Scalar‘𝑄)) ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
42 | 28, 41 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (𝑍 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
43 | 22, 42 | sylan9eqr 2666 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍) → (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
44 | | csbov12g 6587 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐷 → ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) = (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) = (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
46 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
(⦋𝑑 /
𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) ∈ V |
47 | 45, 46 | syl6eqel 2696 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) ∈ V) |
48 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) = (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) |
49 | 48 | fvmpts 6194 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝐷 ∧ ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) ∈ V) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊)) |
50 | 12, 47, 49 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊)) |
51 | 50, 45 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
52 | 51 | eqeq1d 2612 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 ↔
(⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 )) |
53 | 52 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍) → (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 ↔
(⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 )) |
54 | 43, 53 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 ) |
55 | 54 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (⦋𝑑 / 𝑘⦌𝑆 = 𝑍 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 )) |
56 | 21, 55 | sylbid 229 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = 𝑍 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 )) |
57 | 56 | necon3d 2803 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 → ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍)) |
58 | 57 | ss2rabdv 3646 |
. . 3
⊢ (𝜑 → {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 } ⊆ {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍}) |
59 | | ovex 6577 |
. . . . . 6
⊢ (𝑆 ∗ 𝑊) ∈ V |
60 | 59 | rgenw 2908 |
. . . . 5
⊢
∀𝑘 ∈
𝐷 (𝑆 ∗ 𝑊) ∈ V |
61 | 48 | fnmpt 5933 |
. . . . 5
⊢
(∀𝑘 ∈
𝐷 (𝑆 ∗ 𝑊) ∈ V → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) Fn 𝐷) |
62 | 60, 61 | mp1i 13 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) Fn 𝐷) |
63 | | suppvalfn 7189 |
. . . 4
⊢ (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 }) |
64 | 62, 1, 9, 63 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 }) |
65 | 18 | fnmpt 5933 |
. . . . 5
⊢
(∀𝑘 ∈
𝐷 𝑆 ∈ 𝐵 → (𝑘 ∈ 𝐷 ↦ 𝑆) Fn 𝐷) |
66 | 14, 65 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ 𝑆) Fn 𝐷) |
67 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑅) ∈ V |
68 | 23, 67 | eqeltri 2684 |
. . . . 5
⊢ 𝑍 ∈ V |
69 | 68 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ V) |
70 | | suppvalfn 7189 |
. . . 4
⊢ (((𝑘 ∈ 𝐷 ↦ 𝑆) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 𝑍 ∈ V) → ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍}) |
71 | 66, 1, 69, 70 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍}) |
72 | 58, 64, 71 | 3sstr4d 3611 |
. 2
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) ⊆ ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍)) |
73 | | suppssfifsupp 8173 |
. 2
⊢ ((((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) ∈ V ∧ Fun (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) ∧ 0 ∈ V) ∧ (((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) ∈ Fin ∧ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) ⊆ ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍))) → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) finSupp 0 ) |
74 | 3, 5, 9, 11, 72, 73 | syl32anc 1326 |
1
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) finSupp 0 ) |