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 → 𝐷 : 𝐵𝐾 )