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 ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetf.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion mdetf ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ 𝐾 )

Proof

Step Hyp Ref Expression
1 mdetf.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 mdetf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mdetf.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 5 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → 𝑅 ∈ Ring )
7 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
8 6 7 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → 𝑅 ∈ CMnd )
9 2 3 matrcl ⊢ ( 𝑚 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
10 9 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
11 10 simpld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → 𝑁 ∈ Fin )
12 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
13 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
14 12 13 symgbasfi ⊢ ( 𝑁 ∈ Fin → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
15 11 14 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
16 5 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
17 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
18 6 11 17 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
19 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
20 19 4 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
21 13 20 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
22 18 21 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
23 22 ffvelrnda ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝐾 )
24 19 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
25 24 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
26 11 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑁 ∈ Fin )
27 2 4 3 matbas2i ⊢ ( 𝑚 ∈ 𝐵 → 𝑚 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
28 27 ad3antlr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → 𝑚 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
29 elmapi ⊢ ( 𝑚 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) → 𝑚 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
30 28 29 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → 𝑚 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
31 12 13 symgbasf ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) → 𝑝 : 𝑁 ⟶ 𝑁 )
32 31 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑝 : 𝑁 ⟶ 𝑁 )
33 32 ffvelrnda ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑐 ) ∈ 𝑁 )
34 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
35 30 33 34 fovrnd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ∈ 𝐾 )
36 35 ralrimiva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ∀ 𝑐 ∈ 𝑁 ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ∈ 𝐾 )
37 20 25 26 36 gsummptcl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ) ) ∈ 𝐾 )
38 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
39 4 38 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝐾 ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ) ) ∈ 𝐾 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ) ) ) ∈ 𝐾 )
40 16 23 37 39 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ) ) ) ∈ 𝐾 )
41 40 ralrimiva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ∀ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ) ) ) ∈ 𝐾 )
42 4 8 15 41 gsummptcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵 ) → ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ) ) ) ) ) ∈ 𝐾 )
43 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
44 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
45 1 2 3 13 43 44 38 19 mdetfval ⊢ 𝐷 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑐 ) 𝑚 𝑐 ) ) ) ) ) ) )
46 42 45 fmptd ⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ 𝐾 )