Metamath Proof Explorer

Theorem smadiadetlem0

Description: Lemma 0 for smadiadet : The products 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 )
Assertion smadiadetlem0 
|- ( ( M e. B /\ K e. N /\ L e. N ) -> ( Q 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 ) ) ) ( Q ` 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 3 a1i 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> R e. CRing )
9 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
10 9 simpld 
 |-  ( M e. B -> N e. Fin )
11 10 3ad2ant1 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> N e. Fin )
12 11 adantr 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> N e. Fin )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 3 13 mp1i 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> R e. Ring )
15 eldifi 
 |-  ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> Q e. P )
16 15 adantl 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> Q e. P )
17 1 2 3 4 5 marep01ma 
 |-  ( M e. B -> ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) e. B )
18 17 3ad2ant1 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) e. B )
19 18 adantr 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) e. B )
20 1 2 6 matepm2cl 
 |-  ( ( R e. Ring /\ Q e. P /\ ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) e. B ) -> A. m e. N ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) e. ( Base ` R ) )
21 14 16 19 20 syl3anc 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> A. m e. N ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) e. ( Base ` R ) )
22 id 
 |-  ( m = n -> m = n )
23 fveq2 
 |-  ( m = n -> ( Q ` m ) = ( Q ` n ) )
24 22 23 oveq12d 
 |-  ( m = n -> ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) = ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) )
25 24 eleq1d 
 |-  ( m = n -> ( ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) e. ( Base ` R ) <-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) e. ( Base ` R ) ) )
26 25 rspccv 
 |-  ( A. m e. N ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) e. ( Base ` R ) -> ( n e. N -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) e. ( Base ` R ) ) )
27 21 26 syl 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( n e. N -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) e. ( Base ` R ) ) )
28 27 imp 
 |-  ( ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ n e. N ) -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) e. ( Base ` R ) )
29 id 
 |-  ( n = m -> n = m )
30 fveq2 
 |-  ( n = m -> ( Q ` n ) = ( Q ` m ) )
31 29 30 oveq12d 
 |-  ( n = m -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) = ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) )
32 31 adantl 
 |-  ( ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ n = m ) -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) = ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) )
33 6 4 5 symgmatr01 
 |-  ( ( K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. m e. N ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) = .0. ) )
34 33 3adant1 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. m e. N ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) = .0. ) )
35 34 imp 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> E. m e. N ( m ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` m ) ) = .0. )
36 7 4 8 12 28 32 35 gsummgp0 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ Q 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 ) ) ) ( Q ` n ) ) ) ) = .0. )
37 36 ex 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( Q 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 ) ) ) ( Q ` n ) ) ) ) = .0. ) )