Metamath Proof Explorer


Theorem gsumsplit2

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumsplit2.b 𝐵 = ( Base ‘ 𝐺 )
gsumsplit2.z 0 = ( 0g𝐺 )
gsumsplit2.p + = ( +g𝐺 )
gsumsplit2.g ( 𝜑𝐺 ∈ CMnd )
gsumsplit2.a ( 𝜑𝐴𝑉 )
gsumsplit2.f ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
gsumsplit2.w ( 𝜑 → ( 𝑘𝐴𝑋 ) finSupp 0 )
gsumsplit2.i ( 𝜑 → ( 𝐶𝐷 ) = ∅ )
gsumsplit2.u ( 𝜑𝐴 = ( 𝐶𝐷 ) )
Assertion gsumsplit2 ( 𝜑 → ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘𝐶𝑋 ) ) + ( 𝐺 Σg ( 𝑘𝐷𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumsplit2.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumsplit2.z 0 = ( 0g𝐺 )
3 gsumsplit2.p + = ( +g𝐺 )
4 gsumsplit2.g ( 𝜑𝐺 ∈ CMnd )
5 gsumsplit2.a ( 𝜑𝐴𝑉 )
6 gsumsplit2.f ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
7 gsumsplit2.w ( 𝜑 → ( 𝑘𝐴𝑋 ) finSupp 0 )
8 gsumsplit2.i ( 𝜑 → ( 𝐶𝐷 ) = ∅ )
9 gsumsplit2.u ( 𝜑𝐴 = ( 𝐶𝐷 ) )
10 6 fmpttd ( 𝜑 → ( 𝑘𝐴𝑋 ) : 𝐴𝐵 )
11 1 2 3 4 5 10 7 8 9 gsumsplit ( 𝜑 → ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) = ( ( 𝐺 Σg ( ( 𝑘𝐴𝑋 ) ↾ 𝐶 ) ) + ( 𝐺 Σg ( ( 𝑘𝐴𝑋 ) ↾ 𝐷 ) ) ) )
12 ssun1 𝐶 ⊆ ( 𝐶𝐷 )
13 12 9 sseqtrrid ( 𝜑𝐶𝐴 )
14 13 resmptd ( 𝜑 → ( ( 𝑘𝐴𝑋 ) ↾ 𝐶 ) = ( 𝑘𝐶𝑋 ) )
15 14 oveq2d ( 𝜑 → ( 𝐺 Σg ( ( 𝑘𝐴𝑋 ) ↾ 𝐶 ) ) = ( 𝐺 Σg ( 𝑘𝐶𝑋 ) ) )
16 ssun2 𝐷 ⊆ ( 𝐶𝐷 )
17 16 9 sseqtrrid ( 𝜑𝐷𝐴 )
18 17 resmptd ( 𝜑 → ( ( 𝑘𝐴𝑋 ) ↾ 𝐷 ) = ( 𝑘𝐷𝑋 ) )
19 18 oveq2d ( 𝜑 → ( 𝐺 Σg ( ( 𝑘𝐴𝑋 ) ↾ 𝐷 ) ) = ( 𝐺 Σg ( 𝑘𝐷𝑋 ) ) )
20 15 19 oveq12d ( 𝜑 → ( ( 𝐺 Σg ( ( 𝑘𝐴𝑋 ) ↾ 𝐶 ) ) + ( 𝐺 Σg ( ( 𝑘𝐴𝑋 ) ↾ 𝐷 ) ) ) = ( ( 𝐺 Σg ( 𝑘𝐶𝑋 ) ) + ( 𝐺 Σg ( 𝑘𝐷𝑋 ) ) ) )
21 11 20 eqtrd ( 𝜑 → ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘𝐶𝑋 ) ) + ( 𝐺 Σg ( 𝑘𝐷𝑋 ) ) ) )