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 ∈ 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 ∈ CRing → R ∈ Ring
6 5 adantr ⊢ R ∈ CRing ∧ m ∈ B → R ∈ Ring
7 ringcmn ⊢ R ∈ Ring → R ∈ CMnd
8 6 7 syl ⊢ R ∈ CRing ∧ m ∈ B → R ∈ CMnd
9 2 3 matrcl ⊢ m ∈ B → N ∈ Fin ∧ R ∈ V
10 9 adantl ⊢ R ∈ CRing ∧ m ∈ B → N ∈ Fin ∧ R ∈ V
11 10 simpld ⊢ R ∈ CRing ∧ m ∈ B → N ∈ Fin
12 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
13 eqid ⊢ Base SymGrp ⁡ N = Base SymGrp ⁡ N
14 12 13 symgbasfi ⊢ N ∈ Fin → Base SymGrp ⁡ N ∈ Fin
15 11 14 syl ⊢ R ∈ CRing ∧ m ∈ B → Base SymGrp ⁡ N ∈ Fin
16 5 ad2antrr ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → R ∈ Ring
17 zrhpsgnmhm ⊢ R ∈ Ring ∧ N ∈ Fin → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R
18 6 11 17 syl2anc ⊢ R ∈ CRing ∧ m ∈ B → ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R
19 eqid ⊢ mulGrp R = mulGrp R
20 19 4 mgpbas ⊢ K = Base mulGrp R
21 13 20 mhmf ⊢ ℤRHom ⁡ R ∘ pmSgn ⁡ N ∈ SymGrp ⁡ N MndHom mulGrp R → ℤRHom ⁡ R ∘ pmSgn ⁡ N : Base SymGrp ⁡ N ⟶ K
22 18 21 syl ⊢ R ∈ CRing ∧ m ∈ B → ℤRHom ⁡ R ∘ pmSgn ⁡ N : Base SymGrp ⁡ N ⟶ K
23 22 ffvelrnda ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ∈ K
24 19 crngmgp ⊢ R ∈ CRing → mulGrp R ∈ CMnd
25 24 ad2antrr ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → mulGrp R ∈ CMnd
26 11 adantr ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → N ∈ Fin
27 2 4 3 matbas2i ⊢ m ∈ B → m ∈ K N × N
28 27 ad3antlr ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N ∧ c ∈ N → m ∈ K N × N
29 elmapi ⊢ m ∈ K N × N → m : N × N ⟶ K
30 28 29 syl ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N ∧ c ∈ N → m : N × N ⟶ K
31 12 13 symgbasf ⊢ p ∈ Base SymGrp ⁡ N → p : N ⟶ N
32 31 adantl ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → p : N ⟶ N
33 32 ffvelrnda ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N ∧ c ∈ N → p ⁡ c ∈ N
34 simpr ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N ∧ c ∈ N → c ∈ N
35 30 33 34 fovrnd ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N ∧ c ∈ N → p ⁡ c m c ∈ K
36 35 ralrimiva ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → ∀ c ∈ N p ⁡ c m c ∈ K
37 20 25 26 36 gsummptcl ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → ∑ mulGrp R c ∈ N p ⁡ c m c ∈ K
38 eqid ⊢ ⋅ R = ⋅ R
39 4 38 ringcl ⊢ R ∈ Ring ∧ ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ∈ K ∧ ∑ mulGrp R c ∈ N p ⁡ c m c ∈ K → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R c ∈ N p ⁡ c m c ∈ K
40 16 23 37 39 syl3anc ⊢ R ∈ CRing ∧ m ∈ B ∧ p ∈ Base SymGrp ⁡ N → ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R c ∈ N p ⁡ c m c ∈ K
41 40 ralrimiva ⊢ R ∈ CRing ∧ m ∈ B → ∀ p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R c ∈ N p ⁡ c m c ∈ K
42 4 8 15 41 gsummptcl ⊢ R ∈ CRing ∧ m ∈ B → ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R c ∈ N p ⁡ c m c ∈ K
43 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
44 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
45 1 2 3 13 43 44 38 19 mdetfval ⊢ D = m ∈ B ⟼ ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R c ∈ N p ⁡ c m c
46 42 45 fmptd ⊢ R ∈ CRing → D : B ⟶ K