Step | Hyp | Ref
| Expression |
1 | | lcomfsupp.j |
. . . 4
⊢ (𝜑 → 𝐺 finSupp 𝑌) |
2 | 1 | fsuppimpd 8165 |
. . 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 18725 |
. . . 4
⊢ (𝜑 → (𝐺 ∘𝑓 · 𝐻):𝐼⟶𝐵) |
12 | | eldifi 3694 |
. . . . . 6
⊢ (𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌)) → 𝑥 ∈ 𝐼) |
13 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐺:𝐼⟶𝐾 → 𝐺 Fn 𝐼) |
14 | 8, 13 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn 𝐼) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺 Fn 𝐼) |
16 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐻:𝐼⟶𝐵 → 𝐻 Fn 𝐼) |
17 | 9, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 Fn 𝐼) |
18 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐻 Fn 𝐼) |
19 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉) |
20 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
21 | | fnfvof 6809 |
. . . . . . 7
⊢ (((𝐺 Fn 𝐼 ∧ 𝐻 Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼)) → ((𝐺 ∘𝑓 · 𝐻)‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑥))) |
22 | 15, 18, 19, 20, 21 | syl22anc 1319 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐺 ∘𝑓 · 𝐻)‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑥))) |
23 | 12, 22 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → ((𝐺 ∘𝑓 · 𝐻)‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑥))) |
24 | | ssid 3587 |
. . . . . . . 8
⊢ (𝐺 supp 𝑌) ⊆ (𝐺 supp 𝑌) |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐺 supp 𝑌) ⊆ (𝐺 supp 𝑌)) |
26 | | lcomfsupp.y |
. . . . . . . . 9
⊢ 𝑌 = (0g‘𝐹) |
27 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝐹) ∈ V |
28 | 26, 27 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑌 ∈ V |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) |
30 | 8, 25, 10, 29 | suppssr 7213 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → (𝐺‘𝑥) = 𝑌) |
31 | 30 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → ((𝐺‘𝑥) · (𝐻‘𝑥)) = (𝑌 · (𝐻‘𝑥))) |
32 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑊 ∈ LMod) |
33 | 9 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐻‘𝑥) ∈ 𝐵) |
34 | | lcomfsupp.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑊) |
35 | 6, 3, 5, 26, 34 | lmod0vs 18719 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝐻‘𝑥) ∈ 𝐵) → (𝑌 · (𝐻‘𝑥)) = 0 ) |
36 | 32, 33, 35 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑌 · (𝐻‘𝑥)) = 0 ) |
37 | 12, 36 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → (𝑌 · (𝐻‘𝑥)) = 0 ) |
38 | 23, 31, 37 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ (𝐺 supp 𝑌))) → ((𝐺 ∘𝑓 · 𝐻)‘𝑥) = 0 ) |
39 | 11, 38 | suppss 7212 |
. . 3
⊢ (𝜑 → ((𝐺 ∘𝑓 · 𝐻) supp 0 ) ⊆ (𝐺 supp 𝑌)) |
40 | | ssfi 8065 |
. . 3
⊢ (((𝐺 supp 𝑌) ∈ Fin ∧ ((𝐺 ∘𝑓 · 𝐻) supp 0 ) ⊆ (𝐺 supp 𝑌)) → ((𝐺 ∘𝑓 · 𝐻) supp 0 ) ∈
Fin) |
41 | 2, 39, 40 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐺 ∘𝑓 · 𝐻) supp 0 ) ∈
Fin) |
42 | | inidm 3784 |
. . . . 5
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
43 | 14, 17, 10, 10, 42 | offn 6806 |
. . . 4
⊢ (𝜑 → (𝐺 ∘𝑓 · 𝐻) Fn 𝐼) |
44 | | fnfun 5902 |
. . . 4
⊢ ((𝐺 ∘𝑓
·
𝐻) Fn 𝐼 → Fun (𝐺 ∘𝑓 · 𝐻)) |
45 | 43, 44 | syl 17 |
. . 3
⊢ (𝜑 → Fun (𝐺 ∘𝑓 · 𝐻)) |
46 | | ovex 6577 |
. . . 4
⊢ (𝐺 ∘𝑓
·
𝐻) ∈
V |
47 | 46 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐺 ∘𝑓 · 𝐻) ∈ V) |
48 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝑊) ∈ V |
49 | 34, 48 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
50 | 49 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
51 | | funisfsupp 8163 |
. . 3
⊢ ((Fun
(𝐺
∘𝑓 · 𝐻) ∧ (𝐺 ∘𝑓 · 𝐻) ∈ V ∧ 0 ∈ V)
→ ((𝐺
∘𝑓 · 𝐻) finSupp 0 ↔ ((𝐺 ∘𝑓 · 𝐻) supp 0 ) ∈
Fin)) |
52 | 45, 47, 50, 51 | syl3anc 1318 |
. 2
⊢ (𝜑 → ((𝐺 ∘𝑓 · 𝐻) finSupp 0 ↔ ((𝐺 ∘𝑓 · 𝐻) supp 0 ) ∈
Fin)) |
53 | 41, 52 | mpbird 246 |
1
⊢ (𝜑 → (𝐺 ∘𝑓 · 𝐻) finSupp 0 ) |