Theorem gsumdifsnd

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	gsumdifsnd.b	|- B = ( Base ` G )
	gsumdifsnd.p	|- .+ = ( +g ` G )
	gsumdifsnd.g	|- ( ph -> G e. CMnd )
	gsumdifsnd.a	|- ( ph -> A e. W )
	gsumdifsnd.f	|- ( ph -> ( k e. A |-> X ) finSupp ( 0g ` G ) )
	gsumdifsnd.e	|- ( ( ph /\ k e. A ) -> X e. B )
	gsumdifsnd.m	|- ( ph -> M e. A )
	gsumdifsnd.y	|- ( ph -> Y e. B )
	gsumdifsnd.s	|- ( ( ph /\ k = M ) -> X = Y )
Assertion	gsumdifsnd	|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )

Proof

Step	Hyp	Ref	Expression
1		gsumdifsnd.b	|- B = ( Base ` G )
2		gsumdifsnd.p	|- .+ = ( +g ` G )
3		gsumdifsnd.g	|- ( ph -> G e. CMnd )
4		gsumdifsnd.a	|- ( ph -> A e. W )
5		gsumdifsnd.f	|- ( ph -> ( k e. A |-> X ) finSupp ( 0g ` G ) )
6		gsumdifsnd.e	|- ( ( ph /\ k e. A ) -> X e. B )
7		gsumdifsnd.m	|- ( ph -> M e. A )
8		gsumdifsnd.y	|- ( ph -> Y e. B )
9		gsumdifsnd.s	|- ( ( ph /\ k = M ) -> X = Y )
10		eqid	|- ( 0g ` G ) = ( 0g ` G )
11		difid	|- ( { M } \ { M } ) = (/)
12	7	snssd	|- ( ph -> { M } C_ A )
13		difin2	|- ( { M } C_ A -> ( { M } \ { M } ) = ( ( A \ { M } ) i^i { M } ) )
14	12 13	syl	|- ( ph -> ( { M } \ { M } ) = ( ( A \ { M } ) i^i { M } ) )
15	11 14	syl5reqr	|- ( ph -> ( ( A \ { M } ) i^i { M } ) = (/) )
16		difsnid	|- ( M e. A -> ( ( A \ { M } ) u. { M } ) = A )
17	7 16	syl	|- ( ph -> ( ( A \ { M } ) u. { M } ) = A )
18	17	eqcomd	|- ( ph -> A = ( ( A \ { M } ) u. { M } ) )
19	1 10 2 3 4 6 5 15 18	gsumsplit2	|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) )
20		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
21	3 20	syl	|- ( ph -> G e. Mnd )
22	1 21 7 8 9	gsumsnd	|- ( ph -> ( G gsum ( k e. { M } |-> X ) ) = Y )
23	22	oveq2d	|- ( ph -> ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )
24	19 23	eqtrd	|- ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( G gsum ( k e. ( A \ { M } ) |-> X ) ) .+ Y ) )