Metamath Proof Explorer

Theorem madetsumid

Description: The identity summand in the Leibniz' formula of a determinant for a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018)

Ref Expression
Hypotheses madetsumid.a 
|- A = ( N Mat R )
madetsumid.b 
|- B = ( Base ` A )
madetsumid.u 
|- U = ( mulGrp ` R )
madetsumid.y 
|- Y = ( ZRHom ` R )
madetsumid.s 
|- S = ( pmSgn ` N )
madetsumid.t 
|- .x. = ( .r ` R )
Assertion madetsumid 
|- ( ( R e. CRing /\ M e. B /\ P = ( _I |` N ) ) -> ( ( ( Y o. S ) ` P ) .x. ( U gsum ( r e. N |-> ( ( P ` r ) M r ) ) ) ) = ( U gsum ( r e. N |-> ( r M r ) ) ) )

Proof

Step Hyp Ref Expression
1 madetsumid.a 
 |-  A = ( N Mat R )
2 madetsumid.b 
 |-  B = ( Base ` A )
3 madetsumid.u 
 |-  U = ( mulGrp ` R )
4 madetsumid.y 
 |-  Y = ( ZRHom ` R )
5 madetsumid.s 
 |-  S = ( pmSgn ` N )
6 madetsumid.t 
 |-  .x. = ( .r ` R )
7 fveq2 
 |-  ( P = ( _I |` N ) -> ( ( Y o. S ) ` P ) = ( ( Y o. S ) ` ( _I |` N ) ) )
8 fveq1 
 |-  ( P = ( _I |` N ) -> ( P ` r ) = ( ( _I |` N ) ` r ) )
9 8 oveq1d 
 |-  ( P = ( _I |` N ) -> ( ( P ` r ) M r ) = ( ( ( _I |` N ) ` r ) M r ) )
10 9 mpteq2dv 
 |-  ( P = ( _I |` N ) -> ( r e. N |-> ( ( P ` r ) M r ) ) = ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) )
11 10 oveq2d 
 |-  ( P = ( _I |` N ) -> ( U gsum ( r e. N |-> ( ( P ` r ) M r ) ) ) = ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) )
12 7 11 oveq12d 
 |-  ( P = ( _I |` N ) -> ( ( ( Y o. S ) ` P ) .x. ( U gsum ( r e. N |-> ( ( P ` r ) M r ) ) ) ) = ( ( ( Y o. S ) ` ( _I |` N ) ) .x. ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) ) )
13 12 3ad2ant3 
 |-  ( ( R e. CRing /\ M e. B /\ P = ( _I |` N ) ) -> ( ( ( Y o. S ) ` P ) .x. ( U gsum ( r e. N |-> ( ( P ` r ) M r ) ) ) ) = ( ( ( Y o. S ) ` ( _I |` N ) ) .x. ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) ) )
14 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
15 14 simpld 
 |-  ( M e. B -> N e. Fin )
16 4 5 coeq12i 
 |-  ( Y o. S ) = ( ( ZRHom ` R ) o. ( pmSgn ` N ) )
17 16 a1i 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( Y o. S ) = ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) )
18 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
19 18 symgid 
 |-  ( N e. Fin -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
20 19 adantl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
21 17 20 fveq12d 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( Y o. S ) ` ( _I |` N ) ) = ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) )
22 crngring 
 |-  ( R e. CRing -> R e. Ring )
23 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
24 3 oveq2i 
 |-  ( ( SymGrp ` N ) MndHom U ) = ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) )
25 23 24 eleqtrrdi 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom U ) )
26 22 25 sylan 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom U ) )
27 eqid 
 |-  ( 0g ` ( SymGrp ` N ) ) = ( 0g ` ( SymGrp ` N ) )
28 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
29 3 28 ringidval 
 |-  ( 1r ` R ) = ( 0g ` U )
30 27 29 mhm0 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom U ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = ( 1r ` R ) )
31 26 30 syl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` ( 0g ` ( SymGrp ` N ) ) ) = ( 1r ` R ) )
32 21 31 eqtrd 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( Y o. S ) ` ( _I |` N ) ) = ( 1r ` R ) )
33 fvresi 
 |-  ( r e. N -> ( ( _I |` N ) ` r ) = r )
34 33 adantl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ r e. N ) -> ( ( _I |` N ) ` r ) = r )
35 34 oveq1d 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ r e. N ) -> ( ( ( _I |` N ) ` r ) M r ) = ( r M r ) )
36 35 mpteq2dva 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) = ( r e. N |-> ( r M r ) ) )
37 36 oveq2d 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) = ( U gsum ( r e. N |-> ( r M r ) ) ) )
38 32 37 oveq12d 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( ( Y o. S ) ` ( _I |` N ) ) .x. ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) ) = ( ( 1r ` R ) .x. ( U gsum ( r e. N |-> ( r M r ) ) ) ) )
39 15 38 sylan2 
 |-  ( ( R e. CRing /\ M e. B ) -> ( ( ( Y o. S ) ` ( _I |` N ) ) .x. ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) ) = ( ( 1r ` R ) .x. ( U gsum ( r e. N |-> ( r M r ) ) ) ) )
40 1 2 3 matgsumcl 
 |-  ( ( R e. CRing /\ M e. B ) -> ( U gsum ( r e. N |-> ( r M r ) ) ) e. ( Base ` R ) )
41 eqid 
 |-  ( Base ` R ) = ( Base ` R )
42 41 6 28 ringlidm 
 |-  ( ( R e. Ring /\ ( U gsum ( r e. N |-> ( r M r ) ) ) e. ( Base ` R ) ) -> ( ( 1r ` R ) .x. ( U gsum ( r e. N |-> ( r M r ) ) ) ) = ( U gsum ( r e. N |-> ( r M r ) ) ) )
43 22 40 42 syl2an2r 
 |-  ( ( R e. CRing /\ M e. B ) -> ( ( 1r ` R ) .x. ( U gsum ( r e. N |-> ( r M r ) ) ) ) = ( U gsum ( r e. N |-> ( r M r ) ) ) )
44 39 43 eqtrd 
 |-  ( ( R e. CRing /\ M e. B ) -> ( ( ( Y o. S ) ` ( _I |` N ) ) .x. ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) ) = ( U gsum ( r e. N |-> ( r M r ) ) ) )
45 44 3adant3 
 |-  ( ( R e. CRing /\ M e. B /\ P = ( _I |` N ) ) -> ( ( ( Y o. S ) ` ( _I |` N ) ) .x. ( U gsum ( r e. N |-> ( ( ( _I |` N ) ` r ) M r ) ) ) ) = ( U gsum ( r e. N |-> ( r M r ) ) ) )
46 13 45 eqtrd 
 |-  ( ( R e. CRing /\ M e. B /\ P = ( _I |` N ) ) -> ( ( ( Y o. S ) ` P ) .x. ( U gsum ( r e. N |-> ( ( P ` r ) M r ) ) ) ) = ( U gsum ( r e. N |-> ( r M r ) ) ) )