Theorem smadiadetlem2

Description: Lemma 2 for smadiadet : The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to itself. (Contributed by AV, 31-Dec-2018)

	Ref	Expression
Hypotheses	marep01ma.a	|- A = ( N Mat R )
	marep01ma.b	|- B = ( Base ` A )
	marep01ma.r	|- R e. CRing
	marep01ma.0	|- .0. = ( 0g ` R )
	marep01ma.1	|- .1. = ( 1r ` R )
	smadiadetlem.p	|- P = ( Base ` ( SymGrp ` N ) )
	smadiadetlem.g	|- G = ( mulGrp ` R )
	madetminlem.y	|- Y = ( ZRHom ` R )
	madetminlem.s	|- S = ( pmSgn ` N )
	madetminlem.t	|- .x. = ( .r ` R )
Assertion	smadiadetlem2	|- ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = K } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	|- A = ( N Mat R )
2		marep01ma.b	|- B = ( Base ` A )
3		marep01ma.r	|- R e. CRing
4		marep01ma.0	|- .0. = ( 0g ` R )
5		marep01ma.1	|- .1. = ( 1r ` R )
6		smadiadetlem.p	|- P = ( Base ` ( SymGrp ` N ) )
7		smadiadetlem.g	|- G = ( mulGrp ` R )
8		madetminlem.y	|- Y = ( ZRHom ` R )
9		madetminlem.s	|- S = ( pmSgn ` N )
10		madetminlem.t	|- .x. = ( .r ` R )
11	1 2 3 4 5 6 7 8 9 10	smadiadetlem1a	|- ( ( M e. B /\ K e. N /\ K e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = K } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = .0. )
12	11	3anidm23	|- ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = K } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = .0. )