Metamath Proof Explorer

Theorem mdetf

Description: Functionality of the determinant, see also definition in Lang p. 513. (Contributed by Stefan O'Rear, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mdetf.d 
|- D = ( N maDet R )
mdetf.a 
|- A = ( N Mat R )
mdetf.b 
|- B = ( Base ` A )
mdetf.k 
|- K = ( Base ` R )
Assertion mdetf 
|- ( R e. CRing -> D : B --> K )

Proof

Step Hyp Ref Expression
1 mdetf.d 
 |-  D = ( N maDet R )
2 mdetf.a 
 |-  A = ( N Mat R )
3 mdetf.b 
 |-  B = ( Base ` A )
4 mdetf.k 
 |-  K = ( Base ` R )
5 crngring 
 |-  ( R e. CRing -> R e. Ring )
6 5 adantr 
 |-  ( ( R e. CRing /\ m e. B ) -> R e. Ring )
7 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
8 6 7 syl 
 |-  ( ( R e. CRing /\ m e. B ) -> R e. CMnd )
9 2 3 matrcl 
 |-  ( m e. B -> ( N e. Fin /\ R e. _V ) )
10 9 adantl 
 |-  ( ( R e. CRing /\ m e. B ) -> ( N e. Fin /\ R e. _V ) )
11 10 simpld 
 |-  ( ( R e. CRing /\ m e. B ) -> N e. Fin )
12 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
13 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
14 12 13 symgbasfi 
 |-  ( N e. Fin -> ( Base ` ( SymGrp ` N ) ) e. Fin )
15 11 14 syl 
 |-  ( ( R e. CRing /\ m e. B ) -> ( Base ` ( SymGrp ` N ) ) e. Fin )
16 5 ad2antrr 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> R e. Ring )
17 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
18 6 11 17 syl2anc 
 |-  ( ( R e. CRing /\ m e. B ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
19 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
20 19 4 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
21 13 20 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
22 18 21 syl 
 |-  ( ( R e. CRing /\ m e. B ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
23 22 ffvelrnda 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. K )
24 19 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
25 24 ad2antrr 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( mulGrp ` R ) e. CMnd )
26 11 adantr 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> N e. Fin )
27 2 4 3 matbas2i 
 |-  ( m e. B -> m e. ( K ^m ( N X. N ) ) )
28 27 ad3antlr 
 |-  ( ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> m e. ( K ^m ( N X. N ) ) )
29 elmapi 
 |-  ( m e. ( K ^m ( N X. N ) ) -> m : ( N X. N ) --> K )
30 28 29 syl 
 |-  ( ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> m : ( N X. N ) --> K )
31 12 13 symgbasf 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) -> p : N --> N )
32 31 adantl 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> p : N --> N )
33 32 ffvelrnda 
 |-  ( ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> ( p ` c ) e. N )
34 simpr 
 |-  ( ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> c e. N )
35 30 33 34 fovrnd 
 |-  ( ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ c e. N ) -> ( ( p ` c ) m c ) e. K )
36 35 ralrimiva 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> A. c e. N ( ( p ` c ) m c ) e. K )
37 20 25 26 36 gsummptcl 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( mulGrp ` R ) gsum ( c e. N |-> ( ( p ` c ) m c ) ) ) e. K )
38 eqid 
 |-  ( .r ` R ) = ( .r ` R )
39 4 38 ringcl 
 |-  ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) e. K /\ ( ( mulGrp ` R ) gsum ( c e. N |-> ( ( p ` c ) m c ) ) ) e. K ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( c e. N |-> ( ( p ` c ) m c ) ) ) ) e. K )
40 16 23 37 39 syl3anc 
 |-  ( ( ( R e. CRing /\ m e. B ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( c e. N |-> ( ( p ` c ) m c ) ) ) ) e. K )
41 40 ralrimiva 
 |-  ( ( R e. CRing /\ m e. B ) -> A. p e. ( Base ` ( SymGrp ` N ) ) ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( c e. N |-> ( ( p ` c ) m c ) ) ) ) e. K )
42 4 8 15 41 gsummptcl 
 |-  ( ( R e. CRing /\ m e. B ) -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( c e. N |-> ( ( p ` c ) m c ) ) ) ) ) ) e. K )
43 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
44 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
45 1 2 3 13 43 44 38 19 mdetfval 
 |-  D = ( m e. B |-> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( c e. N |-> ( ( p ` c ) m c ) ) ) ) ) ) )
46 42 45 fmptd 
 |-  ( R e. CRing -> D : B --> K )