This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsummptfssub

Description: The difference of two group sums expressed as mappings. (Contributed by AV, 7-Nov-2019)

Ref Expression
Hypotheses gsummptfssub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfssub.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsummptfssub.s ⊢ − = ( -g ‘ 𝐺 )
gsummptfssub.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
gsummptfssub.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsummptfssub.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
gsummptfssub.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
gsummptfssub.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
gsummptfssub.h ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
gsummptfssub.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
gsummptfssub.v ⊢ ( 𝜑 → 𝐻 finSupp 0 )
Assertion gsummptfssub ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfssub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfssub.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsummptfssub.s ⊢ − = ( -g ‘ 𝐺 )
4 gsummptfssub.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
5 gsummptfssub.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 gsummptfssub.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
7 gsummptfssub.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
8 gsummptfssub.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
9 gsummptfssub.h ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
10 gsummptfssub.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
11 gsummptfssub.v ⊢ ( 𝜑 → 𝐻 finSupp 0 )
12 5 6 7 8 9 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) )
13 12 eqcomd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) = ( 𝐹 ∘f − 𝐻 ) )
14 13 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) ) = ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) )
15 8 6 fmpt3d ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
16 9 7 fmpt3d ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
17 1 2 3 4 5 15 16 10 11 gsumsub ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )
18 14 17 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )