# 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}\mathrm{maDet}{R}$
mdetf.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mdetf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
mdetf.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
Assertion mdetf ${⊢}{R}\in \mathrm{CRing}\to {D}:{B}⟶{K}$

### Proof

Step Hyp Ref Expression
1 mdetf.d ${⊢}{D}={N}\mathrm{maDet}{R}$
2 mdetf.a ${⊢}{A}={N}\mathrm{Mat}{R}$
3 mdetf.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 mdetf.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
5 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
6 5 adantr ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to {R}\in \mathrm{Ring}$
7 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
8 6 7 syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to {R}\in \mathrm{CMnd}$
9 2 3 matrcl ${⊢}{m}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
10 9 adantl ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
11 10 simpld ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to {N}\in \mathrm{Fin}$
12 eqid ${⊢}\mathrm{SymGrp}\left({N}\right)=\mathrm{SymGrp}\left({N}\right)$
13 eqid ${⊢}{\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}$
14 12 13 symgbasfi ${⊢}{N}\in \mathrm{Fin}\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\in \mathrm{Fin}$
15 11 14 syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\in \mathrm{Fin}$
16 5 ad2antrr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to {R}\in \mathrm{Ring}$
17 zrhpsgnmhm ${⊢}\left({R}\in \mathrm{Ring}\wedge {N}\in \mathrm{Fin}\right)\to \mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\in \left(\mathrm{SymGrp}\left({N}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{R}}\right)$
18 6 11 17 syl2anc ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to \mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\in \left(\mathrm{SymGrp}\left({N}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{R}}\right)$
19 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
20 19 4 mgpbas ${⊢}{K}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{R}}}$
21 13 20 mhmf ${⊢}\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\in \left(\mathrm{SymGrp}\left({N}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{R}}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right):{\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}⟶{K}$
22 18 21 syl ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right):{\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}⟶{K}$
23 22 ffvelrnda ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right)\in {K}$
24 19 crngmgp ${⊢}{R}\in \mathrm{CRing}\to {\mathrm{mulGrp}}_{{R}}\in \mathrm{CMnd}$
25 24 ad2antrr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to {\mathrm{mulGrp}}_{{R}}\in \mathrm{CMnd}$
26 11 adantr ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to {N}\in \mathrm{Fin}$
27 2 4 3 matbas2i ${⊢}{m}\in {B}\to {m}\in \left({{K}}^{\left({N}×{N}\right)}\right)$
28 27 ad3antlr ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\wedge {c}\in {N}\right)\to {m}\in \left({{K}}^{\left({N}×{N}\right)}\right)$
29 elmapi ${⊢}{m}\in \left({{K}}^{\left({N}×{N}\right)}\right)\to {m}:{N}×{N}⟶{K}$
30 28 29 syl ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\wedge {c}\in {N}\right)\to {m}:{N}×{N}⟶{K}$
31 12 13 symgbasf ${⊢}{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\to {p}:{N}⟶{N}$
32 31 adantl ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to {p}:{N}⟶{N}$
33 32 ffvelrnda ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\wedge {c}\in {N}\right)\to {p}\left({c}\right)\in {N}$
34 simpr ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\wedge {c}\in {N}\right)\to {c}\in {N}$
35 30 33 34 fovrnd ${⊢}\left(\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\wedge {c}\in {N}\right)\to {p}\left({c}\right){m}{c}\in {K}$
36 35 ralrimiva ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to \forall {c}\in {N}\phantom{\rule{.4em}{0ex}}{p}\left({c}\right){m}{c}\in {K}$
37 20 25 26 36 gsummptcl ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to \underset{{c}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}}\left({p}\left({c}\right){m}{c}\right)\in {K}$
38 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
39 4 38 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right)\in {K}\wedge \underset{{c}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}}\left({p}\left({c}\right){m}{c}\right)\in {K}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{c}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({c}\right){m}{c}\right)\right)\in {K}$
40 16 23 37 39 syl3anc ${⊢}\left(\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\wedge {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\right)\to \left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{c}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({c}\right){m}{c}\right)\right)\in {K}$
41 40 ralrimiva ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to \forall {p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{c}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({c}\right){m}{c}\right)\right)\in {K}$
42 4 8 15 41 gsummptcl ${⊢}\left({R}\in \mathrm{CRing}\wedge {m}\in {B}\right)\to \underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{c}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({c}\right){m}{c}\right)\right)\right)\in {K}$
43 eqid ${⊢}\mathrm{ℤRHom}\left({R}\right)=\mathrm{ℤRHom}\left({R}\right)$
44 eqid ${⊢}\mathrm{pmSgn}\left({N}\right)=\mathrm{pmSgn}\left({N}\right)$
45 1 2 3 13 43 44 38 19 mdetfval ${⊢}{D}=\left({m}\in {B}⟼\underset{{p}\in {\mathrm{Base}}_{\mathrm{SymGrp}\left({N}\right)}}{{\sum }_{{R}}}\left(\left(\mathrm{ℤRHom}\left({R}\right)\circ \mathrm{pmSgn}\left({N}\right)\right)\left({p}\right){\cdot }_{{R}}\left(\underset{{c}\in {N}}{{\sum }_{{\mathrm{mulGrp}}_{{R}}}},\left({p}\left({c}\right){m}{c}\right)\right)\right)\right)$
46 42 45 fmptd ${⊢}{R}\in \mathrm{CRing}\to {D}:{B}⟶{K}$