Theorem gsumdifsndf

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019)

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

Proof

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