Metamath Proof Explorer

Theorem smadiadetlem1a

Description: Lemma 1a 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 the column with the 1. (Contributed by AV, 3-Jan-2019)

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 smadiadetlem1a 
|- ( ( M e. B /\ K e. N /\ L e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .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 smadiadetlem0 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( p e. ( P \ { q e. P | ( q ` K ) = L } ) -> ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) = .0. ) )
12 11 imp 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ p e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) = .0. )
13 12 oveq2d 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ p e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) = ( ( ( Y o. S ) ` p ) .x. .0. ) )
14 13 mpteq2dva 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) = ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. .0. ) ) )
15 14 oveq2d 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. .0. ) ) ) )
16 crngring 
 |-  ( R e. CRing -> R e. Ring )
17 3 16 mp1i 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ p e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> R e. Ring )
18 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
19 18 simpld 
 |-  ( M e. B -> N e. Fin )
20 19 3ad2ant1 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> N e. Fin )
21 20 adantr 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ p e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> N e. Fin )
22 eldifi 
 |-  ( p e. ( P \ { q e. P | ( q ` K ) = L } ) -> p e. P )
23 22 adantl 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ p e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> p e. P )
24 6 9 8 zrhcopsgnelbas 
 |-  ( ( R e. Ring /\ N e. Fin /\ p e. P ) -> ( ( Y o. S ) ` p ) e. ( Base ` R ) )
25 17 21 23 24 syl3anc 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ p e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( ( Y o. S ) ` p ) e. ( Base ` R ) )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 26 10 4 ringrz 
 |-  ( ( R e. Ring /\ ( ( Y o. S ) ` p ) e. ( Base ` R ) ) -> ( ( ( Y o. S ) ` p ) .x. .0. ) = .0. )
28 17 25 27 syl2anc 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ p e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( ( ( Y o. S ) ` p ) .x. .0. ) = .0. )
29 28 mpteq2dva 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. .0. ) ) = ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> .0. ) )
30 29 oveq2d 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. .0. ) ) ) = ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> .0. ) ) )
31 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
32 3 16 31 mp2b 
 |-  R e. Mnd
33 6 fvexi 
 |-  P e. _V
34 difexg 
 |-  ( P e. _V -> ( P \ { q e. P | ( q ` K ) = L } ) e. _V )
35 33 34 mp1i 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( P \ { q e. P | ( q ` K ) = L } ) e. _V )
36 4 gsumz 
 |-  ( ( R e. Mnd /\ ( P \ { q e. P | ( q ` K ) = L } ) e. _V ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> .0. ) ) = .0. )
37 32 35 36 sylancr 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> .0. ) ) = .0. )
38 15 30 37 3eqtrd 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( R gsum ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = .0. )