gsumunsnf

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		gsumunsnf.0	\|- F/_ k Y
2		gsumunsnf.b	\|- B = ( Base ` G )
3		gsumunsnf.p	\|- .+ = ( +g ` G )
4		gsumunsnf.g	\|- ( ph -> G e. CMnd )
5		gsumunsnf.a	\|- ( ph -> A e. Fin )
6		gsumunsnf.f	\|- ( ( ph /\ k e. A ) -> X e. B )
7		gsumunsnf.m	\|- ( ph -> M e. V )
8		gsumunsnf.d	\|- ( ph -> -. M e. A )
9		gsumunsnf.y	\|- ( ph -> Y e. B )
10		gsumunsnf.s	\|- ( k = M -> X = Y )
11	10	adantl	\|- ( ( ph /\ k = M ) -> X = Y )
12	2 3 4 5 6 7 8 9 11 1	gsumunsnfd	\|- ( ph -> ( G gsum ( k e. ( A u. { M } ) \|-> X ) ) = ( ( G gsum ( k e. A \|-> X ) ) .+ Y ) )

Metamath Proof Explorer

Theorem gsumunsnf

Proof