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=NmaDetR
mdetf.a A=NMatR
mdetf.b B=BaseA
mdetf.k K=BaseR
Assertion mdetf RCRingD:BK

Proof

Step Hyp Ref Expression
1 mdetf.d D=NmaDetR
2 mdetf.a A=NMatR
3 mdetf.b B=BaseA
4 mdetf.k K=BaseR
5 crngring RCRingRRing
6 5 adantr RCRingmBRRing
7 ringcmn RRingRCMnd
8 6 7 syl RCRingmBRCMnd
9 2 3 matrcl mBNFinRV
10 9 adantl RCRingmBNFinRV
11 10 simpld RCRingmBNFin
12 eqid SymGrpN=SymGrpN
13 eqid BaseSymGrpN=BaseSymGrpN
14 12 13 symgbasfi NFinBaseSymGrpNFin
15 11 14 syl RCRingmBBaseSymGrpNFin
16 5 ad2antrr RCRingmBpBaseSymGrpNRRing
17 zrhpsgnmhm RRingNFinℤRHomRpmSgnNSymGrpNMndHommulGrpR
18 6 11 17 syl2anc RCRingmBℤRHomRpmSgnNSymGrpNMndHommulGrpR
19 eqid mulGrpR=mulGrpR
20 19 4 mgpbas K=BasemulGrpR
21 13 20 mhmf ℤRHomRpmSgnNSymGrpNMndHommulGrpRℤRHomRpmSgnN:BaseSymGrpNK
22 18 21 syl RCRingmBℤRHomRpmSgnN:BaseSymGrpNK
23 22 ffvelrnda RCRingmBpBaseSymGrpNℤRHomRpmSgnNpK
24 19 crngmgp RCRingmulGrpRCMnd
25 24 ad2antrr RCRingmBpBaseSymGrpNmulGrpRCMnd
26 11 adantr RCRingmBpBaseSymGrpNNFin
27 2 4 3 matbas2i mBmKN×N
28 27 ad3antlr RCRingmBpBaseSymGrpNcNmKN×N
29 elmapi mKN×Nm:N×NK
30 28 29 syl RCRingmBpBaseSymGrpNcNm:N×NK
31 12 13 symgbasf pBaseSymGrpNp:NN
32 31 adantl RCRingmBpBaseSymGrpNp:NN
33 32 ffvelrnda RCRingmBpBaseSymGrpNcNpcN
34 simpr RCRingmBpBaseSymGrpNcNcN
35 30 33 34 fovrnd RCRingmBpBaseSymGrpNcNpcmcK
36 35 ralrimiva RCRingmBpBaseSymGrpNcNpcmcK
37 20 25 26 36 gsummptcl RCRingmBpBaseSymGrpNmulGrpRcNpcmcK
38 eqid R=R
39 4 38 ringcl RRingℤRHomRpmSgnNpKmulGrpRcNpcmcKℤRHomRpmSgnNpRmulGrpRcNpcmcK
40 16 23 37 39 syl3anc RCRingmBpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcmcK
41 40 ralrimiva RCRingmBpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcmcK
42 4 8 15 41 gsummptcl RCRingmBRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcmcK
43 eqid ℤRHomR=ℤRHomR
44 eqid pmSgnN=pmSgnN
45 1 2 3 13 43 44 38 19 mdetfval D=mBRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcmc
46 42 45 fmptd RCRingD:BK