Step |
Hyp |
Ref |
Expression |
1 |
|
tsms0.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
2 |
|
tsms0.1 |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
3 |
|
tsms0.2 |
⊢ ( 𝜑 → 𝐺 ∈ TopSp ) |
4 |
|
tsms0.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
5 |
|
cmnmnd |
⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd ) |
6 |
2 5
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
7 |
1
|
gsumz |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 ) |
8 |
6 4 7
|
syl2anc |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 ) |
9 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
10 |
9 1
|
mndidcl |
⊢ ( 𝐺 ∈ Mnd → 0 ∈ ( Base ‘ 𝐺 ) ) |
11 |
6 10
|
syl |
⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝐺 ) ) |
12 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ( Base ‘ 𝐺 ) ) |
13 |
12
|
fmpttd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 0 ) : 𝐴 ⟶ ( Base ‘ 𝐺 ) ) |
14 |
|
fconstmpt |
⊢ ( 𝐴 × { 0 } ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) |
15 |
1
|
fvexi |
⊢ 0 ∈ V |
16 |
15
|
a1i |
⊢ ( 𝜑 → 0 ∈ V ) |
17 |
4 16
|
fczfsuppd |
⊢ ( 𝜑 → ( 𝐴 × { 0 } ) finSupp 0 ) |
18 |
14 17
|
eqbrtrrid |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 0 ) finSupp 0 ) |
19 |
9 1 2 3 4 13 18
|
tsmsid |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) ∈ ( 𝐺 tsums ( 𝑥 ∈ 𝐴 ↦ 0 ) ) ) |
20 |
8 19
|
eqeltrrd |
⊢ ( 𝜑 → 0 ∈ ( 𝐺 tsums ( 𝑥 ∈ 𝐴 ↦ 0 ) ) ) |