Step | Hyp | Ref
| Expression |
1 | | lcomfsupp.j |
. . . 4
⊢ (𝜑 → 𝐺 finSupp 𝑌) |
2 | 1 | fsuppimpd 8842 |
. . 3
⊢ (𝜑 → (𝐺 supp 𝑌) ∈ Fin) |
3 | | lcomf.f |
. . . . 5
⊢ 𝐹 = (Scalar‘𝑊) |
4 | | lcomf.k |
. . . . 5
⊢ 𝐾 = (Base‘𝐹) |
5 | | lcomf.s |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
6 | | lcomf.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑊) |
7 | | lcomf.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
8 | | lcomf.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝐼⟶𝐾) |
9 | | lcomf.h |
. . . . 5
⊢ (𝜑 → 𝐻:𝐼⟶𝐵) |
10 | | lcomf.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | lcomf 19675 |
. . . 4
⊢ (𝜑 → (𝐺 ∘f · 𝐻):𝐼⟶𝐵) |
12 | | eldifi 4105 |
. . . . . 6
⊢ (𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌)) → 𝑥 ∈ 𝐼) |
13 | 8 | ffnd 6517 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn 𝐼) |
14 | 13 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺 Fn 𝐼) |
15 | 9 | ffnd 6517 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 Fn 𝐼) |
16 | 15 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐻 Fn 𝐼) |
17 | 10 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉) |
18 | | simpr 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
19 | | fnfvof 7425 |
. . . . . . 7
⊢ (((𝐺 Fn 𝐼 ∧ 𝐻 Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼)) → ((𝐺 ∘f · 𝐻)‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑥))) |
20 | 14, 16, 17, 18, 19 | syl22anc 836 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐺 ∘f · 𝐻)‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑥))) |
21 | 12, 20 | sylan2 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → ((𝐺 ∘f · 𝐻)‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑥))) |
22 | | ssidd 3992 |
. . . . . . 7
⊢ (𝜑 → (𝐺 supp 𝑌) ⊆ (𝐺 supp 𝑌)) |
23 | | lcomfsupp.y |
. . . . . . . . 9
⊢ 𝑌 = (0g‘𝐹) |
24 | 23 | fvexi 6686 |
. . . . . . . 8
⊢ 𝑌 ∈ V |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) |
26 | 8, 22, 10, 25 | suppssr 7863 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → (𝐺‘𝑥) = 𝑌) |
27 | 26 | oveq1d 7173 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → ((𝐺‘𝑥) · (𝐻‘𝑥)) = (𝑌 · (𝐻‘𝑥))) |
28 | 9 | ffvelrnda 6853 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐻‘𝑥) ∈ 𝐵) |
29 | | lcomfsupp.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑊) |
30 | 6, 3, 5, 23, 29 | lmod0vs 19669 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝐻‘𝑥) ∈ 𝐵) → (𝑌 · (𝐻‘𝑥)) = 0 ) |
31 | 7, 28, 30 | syl2an2r 683 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑌 · (𝐻‘𝑥)) = 0 ) |
32 | 12, 31 | sylan2 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → (𝑌 · (𝐻‘𝑥)) = 0 ) |
33 | 21, 27, 32 | 3eqtrd 2862 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → ((𝐺 ∘f · 𝐻)‘𝑥) = 0 ) |
34 | 11, 33 | suppss 7862 |
. . 3
⊢ (𝜑 → ((𝐺 ∘f · 𝐻) supp 0 ) ⊆ (𝐺 supp 𝑌)) |
35 | 2, 34 | ssfid 8743 |
. 2
⊢ (𝜑 → ((𝐺 ∘f · 𝐻) supp 0 ) ∈
Fin) |
36 | | inidm 4197 |
. . . . 5
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
37 | 13, 15, 10, 10, 36 | offn 7422 |
. . . 4
⊢ (𝜑 → (𝐺 ∘f · 𝐻) Fn 𝐼) |
38 | | fnfun 6455 |
. . . 4
⊢ ((𝐺 ∘f · 𝐻) Fn 𝐼 → Fun (𝐺 ∘f · 𝐻)) |
39 | 37, 38 | syl 17 |
. . 3
⊢ (𝜑 → Fun (𝐺 ∘f · 𝐻)) |
40 | | ovexd 7193 |
. . 3
⊢ (𝜑 → (𝐺 ∘f · 𝐻) ∈ V) |
41 | 29 | fvexi 6686 |
. . . 4
⊢ 0 ∈
V |
42 | 41 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
43 | | funisfsupp 8840 |
. . 3
⊢ ((Fun
(𝐺 ∘f
·
𝐻) ∧ (𝐺 ∘f · 𝐻) ∈ V ∧ 0 ∈ V) → ((𝐺 ∘f · 𝐻) finSupp 0 ↔ ((𝐺 ∘f · 𝐻) supp 0 ) ∈
Fin)) |
44 | 39, 40, 42, 43 | syl3anc 1367 |
. 2
⊢ (𝜑 → ((𝐺 ∘f · 𝐻) finSupp 0 ↔ ((𝐺 ∘f · 𝐻) supp 0 ) ∈
Fin)) |
45 | 35, 44 | mpbird 259 |
1
⊢ (𝜑 → (𝐺 ∘f · 𝐻) finSupp 0 ) |