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

Metamath Proof Explorer

Theorem gsummptfidmsub

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

Ref Expression
Hypotheses gsummptfidmsub.b 
|- B = ( Base ` G )
gsummptfidmsub.s 
|- .- = ( -g ` G )
gsummptfidmsub.g 
|- ( ph -> G e. Abel )
gsummptfidmsub.a 
|- ( ph -> A e. Fin )
gsummptfidmsub.c 
|- ( ( ph /\ x e. A ) -> C e. B )
gsummptfidmsub.d 
|- ( ( ph /\ x e. A ) -> D e. B )
gsummptfidmsub.f 
|- F = ( x e. A |-> C )
gsummptfidmsub.h 
|- H = ( x e. A |-> D )
Assertion gsummptfidmsub 
|- ( ph -> ( G gsum ( x e. A |-> ( C .- D ) ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfidmsub.b 
 |-  B = ( Base ` G )
2 gsummptfidmsub.s 
 |-  .- = ( -g ` G )
3 gsummptfidmsub.g 
 |-  ( ph -> G e. Abel )
4 gsummptfidmsub.a 
 |-  ( ph -> A e. Fin )
5 gsummptfidmsub.c 
 |-  ( ( ph /\ x e. A ) -> C e. B )
6 gsummptfidmsub.d 
 |-  ( ( ph /\ x e. A ) -> D e. B )
7 gsummptfidmsub.f 
 |-  F = ( x e. A |-> C )
8 gsummptfidmsub.h 
 |-  H = ( x e. A |-> D )
9 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
10 7 a1i 
 |-  ( ph -> F = ( x e. A |-> C ) )
11 8 a1i 
 |-  ( ph -> H = ( x e. A |-> D ) )
12 fvexd 
 |-  ( ph -> ( 0g ` G ) e. _V )
13 7 4 5 12 fsuppmptdm 
 |-  ( ph -> F finSupp ( 0g ` G ) )
14 8 4 6 12 fsuppmptdm 
 |-  ( ph -> H finSupp ( 0g ` G ) )
15 1 9 2 3 4 5 6 10 11 13 14 gsummptfssub 
 |-  ( ph -> ( G gsum ( x e. A |-> ( C .- D ) ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )