Step |
Hyp |
Ref |
Expression |
1 |
|
fisuppov1.1 |
⊢ ( 𝜑 → 𝑍 ∈ 𝑉 ) |
2 |
|
fisuppov1.2 |
⊢ ( 𝜑 → 0 ∈ 𝑋 ) |
3 |
|
fisuppov1.3 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑊 ) |
4 |
|
fisuppov1.4 |
⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 ) |
5 |
|
fisuppov1.5 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑌 ) |
6 |
|
fisuppov1.6 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐸 ) |
7 |
|
fisuppov1.7 |
⊢ ( 𝜑 → 𝐹 finSupp 0 ) |
8 |
|
fisuppov1.8 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 0 𝑂 𝑦 ) = 𝑍 ) |
9 |
3 4
|
ssexd |
⊢ ( 𝜑 → 𝐷 ∈ V ) |
10 |
9
|
mptexd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) ∈ V ) |
11 |
|
funmpt |
⊢ Fun ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) |
12 |
11
|
a1i |
⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) ) |
13 |
6 4
|
feqresmpt |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
14 |
13
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐷 ) supp 0 ) = ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) supp 0 ) ) |
15 |
6 3
|
fexd |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
16 |
|
ressuppss |
⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ 𝑋 ) → ( ( 𝐹 ↾ 𝐷 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
17 |
15 2 16
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐷 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
18 |
14 17
|
eqsstrrd |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
19 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ V ) |
20 |
18 8 19 5 2
|
suppssov1 |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ ( 𝐹 supp 0 ) ) |
21 |
10 1 12 7 20
|
fsuppsssuppgd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) finSupp 𝑍 ) |