Step |
Hyp |
Ref |
Expression |
1 |
|
tsmslem1.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
tsmslem1.s |
⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin ) |
3 |
|
tsmslem1.1 |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
4 |
|
tsmslem1.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑊 ) |
5 |
|
tsmslem1.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
6 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
7 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝐺 ∈ CMnd ) |
8 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 ) |
9 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
10 |
8 2
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
11 |
|
elfpw |
⊢ ( 𝑋 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ) |
12 |
11
|
simplbi |
⊢ ( 𝑋 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑋 ⊆ 𝐴 ) |
13 |
10 12
|
syl |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ 𝐴 ) |
14 |
9 13
|
fssresd |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ 𝐵 ) |
15 |
10
|
elin2d |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ Fin ) |
16 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ V ) |
17 |
14 15 16
|
fdmfifsupp |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ↾ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) ) |
18 |
1 6 7 8 14 17
|
gsumcl |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑋 ) ) ∈ 𝐵 ) |