Database
BASIC ALGEBRAIC STRUCTURES
Groups
Abelian groups
Group sum operation
gsumres
Metamath Proof Explorer
Description: Extend a finite group sum by padding outside with zeroes.
(Contributed by Mario Carneiro , 15-Dec-2014) (Revised by Mario
Carneiro , 24-Apr-2016) (Revised by AV , 3-Jun-2019)
Ref
Expression
Hypotheses
gsumcl.b
⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumcl.z
⊢ 0 = ( 0g ‘ 𝐺 )
gsumcl.g
⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsumcl.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumcl.f
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumres.s
⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 )
gsumres.w
⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion
gsumres
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) )
Proof
Step
Hyp
Ref
Expression
1
gsumcl.b
⊢ 𝐵 = ( Base ‘ 𝐺 )
2
gsumcl.z
⊢ 0 = ( 0g ‘ 𝐺 )
3
gsumcl.g
⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4
gsumcl.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5
gsumcl.f
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6
gsumres.s
⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 )
7
gsumres.w
⊢ ( 𝜑 → 𝐹 finSupp 0 )
8
eqid
⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
9
cmnmnd
⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
10
3 9
syl
⊢ ( 𝜑 → 𝐺 ∈ Mnd )
11
1 8 3 5
cntzcmnf
⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
12
1 2 8 10 4 5 11 6 7
gsumzres
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 Σg 𝐹 ) )