| Step | Hyp | Ref
| Expression |
| 1 | | mptscmfsupp0.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 2 | 1 | mptexd 7244 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) ∈ V) |
| 3 | | funmpt 6604 |
. . 3
⊢ Fun
(𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → Fun (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))) |
| 5 | | mptscmfsupp0.0 |
. . . 4
⊢ 0 =
(0g‘𝑄) |
| 6 | 5 | fvexi 6920 |
. . 3
⊢ 0 ∈
V |
| 7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → 0 ∈ V) |
| 8 | | mptscmfsupp0.f |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ 𝑆) finSupp 𝑍) |
| 9 | 8 | fsuppimpd 9409 |
. 2
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) ∈ Fin) |
| 10 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑑 ∈ 𝐷) |
| 11 | | mptscmfsupp0.s |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑆 ∈ 𝐵) |
| 12 | 11 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ 𝐷 𝑆 ∈ 𝐵) |
| 13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ∀𝑘 ∈ 𝐷 𝑆 ∈ 𝐵) |
| 14 | | rspcsbela 4438 |
. . . . . . . . 9
⊢ ((𝑑 ∈ 𝐷 ∧ ∀𝑘 ∈ 𝐷 𝑆 ∈ 𝐵) → ⦋𝑑 / 𝑘⦌𝑆 ∈ 𝐵) |
| 15 | 10, 13, 14 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌𝑆 ∈ 𝐵) |
| 16 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐷 ↦ 𝑆) = (𝑘 ∈ 𝐷 ↦ 𝑆) |
| 17 | 16 | fvmpts 7019 |
. . . . . . . 8
⊢ ((𝑑 ∈ 𝐷 ∧ ⦋𝑑 / 𝑘⦌𝑆 ∈ 𝐵) → ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = ⦋𝑑 / 𝑘⦌𝑆) |
| 18 | 10, 15, 17 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = ⦋𝑑 / 𝑘⦌𝑆) |
| 19 | 18 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = 𝑍 ↔ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍)) |
| 20 | | oveq1 7438 |
. . . . . . . . 9
⊢
(⦋𝑑 /
𝑘⦌𝑆 = 𝑍 → (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = (𝑍 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
| 21 | | mptscmfsupp0.z |
. . . . . . . . . . . 12
⊢ 𝑍 = (0g‘𝑅) |
| 22 | | mptscmfsupp0.r |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (Scalar‘𝑄)) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑅 = (Scalar‘𝑄)) |
| 24 | 23 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (0g‘𝑅) =
(0g‘(Scalar‘𝑄))) |
| 25 | 21, 24 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑍 = (0g‘(Scalar‘𝑄))) |
| 26 | 25 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (𝑍 ∗
⦋𝑑 / 𝑘⦌𝑊) =
((0g‘(Scalar‘𝑄)) ∗
⦋𝑑 / 𝑘⦌𝑊)) |
| 27 | | mptscmfsupp0.q |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ LMod) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → 𝑄 ∈ LMod) |
| 29 | | mptscmfsupp0.w |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑊 ∈ 𝐾) |
| 30 | 29 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝐷 𝑊 ∈ 𝐾) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ∀𝑘 ∈ 𝐷 𝑊 ∈ 𝐾) |
| 32 | | rspcsbela 4438 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝐷 ∧ ∀𝑘 ∈ 𝐷 𝑊 ∈ 𝐾) → ⦋𝑑 / 𝑘⦌𝑊 ∈ 𝐾) |
| 33 | 10, 31, 32 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌𝑊 ∈ 𝐾) |
| 34 | | mptscmfsupp0.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (Base‘𝑄) |
| 35 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
| 36 | | mptscmfsupp0.m |
. . . . . . . . . . . 12
⊢ ∗ = (
·𝑠 ‘𝑄) |
| 37 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝑄)) =
(0g‘(Scalar‘𝑄)) |
| 38 | 34, 35, 36, 37, 5 | lmod0vs 20893 |
. . . . . . . . . . 11
⊢ ((𝑄 ∈ LMod ∧
⦋𝑑 / 𝑘⦌𝑊 ∈ 𝐾) →
((0g‘(Scalar‘𝑄)) ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
| 39 | 28, 33, 38 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) →
((0g‘(Scalar‘𝑄)) ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
| 40 | 26, 39 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (𝑍 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
| 41 | 20, 40 | sylan9eqr 2799 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍) → (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 ) |
| 42 | | csbov12g 7477 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐷 → ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) = (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
| 43 | 42 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) = (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
| 44 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢
(⦋𝑑 /
𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) ∈ V |
| 45 | 43, 44 | eqeltrdi 2849 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) ∈ V) |
| 46 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) = (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) |
| 47 | 46 | fvmpts 7019 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ 𝐷 ∧ ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊) ∈ V) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊)) |
| 48 | 10, 45, 47 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = ⦋𝑑 / 𝑘⦌(𝑆 ∗ 𝑊)) |
| 49 | 48, 43 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = (⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊)) |
| 50 | 49 | eqeq1d 2739 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 ↔
(⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 )) |
| 51 | 50 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍) → (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 ↔
(⦋𝑑 / 𝑘⦌𝑆 ∗
⦋𝑑 / 𝑘⦌𝑊) = 0 )) |
| 52 | 41, 51 | mpbird 257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / 𝑘⦌𝑆 = 𝑍) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 ) |
| 53 | 52 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (⦋𝑑 / 𝑘⦌𝑆 = 𝑍 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 )) |
| 54 | 19, 53 | sylbid 240 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) = 𝑍 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) = 0 )) |
| 55 | 54 | necon3d 2961 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐷) → (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 → ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍)) |
| 56 | 55 | ss2rabdv 4076 |
. . 3
⊢ (𝜑 → {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 } ⊆ {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍}) |
| 57 | | ovex 7464 |
. . . . . 6
⊢ (𝑆 ∗ 𝑊) ∈ V |
| 58 | 57 | rgenw 3065 |
. . . . 5
⊢
∀𝑘 ∈
𝐷 (𝑆 ∗ 𝑊) ∈ V |
| 59 | 46 | fnmpt 6708 |
. . . . 5
⊢
(∀𝑘 ∈
𝐷 (𝑆 ∗ 𝑊) ∈ V → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) Fn 𝐷) |
| 60 | 58, 59 | mp1i 13 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) Fn 𝐷) |
| 61 | | suppvalfn 8193 |
. . . 4
⊢ (((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 }) |
| 62 | 60, 1, 7, 61 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊))‘𝑑) ≠ 0 }) |
| 63 | 16 | fnmpt 6708 |
. . . . 5
⊢
(∀𝑘 ∈
𝐷 𝑆 ∈ 𝐵 → (𝑘 ∈ 𝐷 ↦ 𝑆) Fn 𝐷) |
| 64 | 12, 63 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ 𝑆) Fn 𝐷) |
| 65 | 21 | fvexi 6920 |
. . . . 5
⊢ 𝑍 ∈ V |
| 66 | 65 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ V) |
| 67 | | suppvalfn 8193 |
. . . 4
⊢ (((𝑘 ∈ 𝐷 ↦ 𝑆) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 𝑍 ∈ V) → ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍}) |
| 68 | 64, 1, 66, 67 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) = {𝑑 ∈ 𝐷 ∣ ((𝑘 ∈ 𝐷 ↦ 𝑆)‘𝑑) ≠ 𝑍}) |
| 69 | 56, 62, 68 | 3sstr4d 4039 |
. 2
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) ⊆ ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍)) |
| 70 | | suppssfifsupp 9420 |
. 2
⊢ ((((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) ∈ V ∧ Fun (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) ∧ 0 ∈ V) ∧ (((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍) ∈ Fin ∧ ((𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) supp 0 ) ⊆ ((𝑘 ∈ 𝐷 ↦ 𝑆) supp 𝑍))) → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) finSupp 0 ) |
| 71 | 2, 4, 7, 9, 69, 70 | syl32anc 1380 |
1
⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) finSupp 0 ) |