Metamath Proof Explorer

Theorem mdetleib

Description: Full substitution of our determinant definition (also known as Leibniz' Formula, expanding by columns). Proposition 4.6 in Lang p. 514. (Contributed by Stefan O'Rear, 3-Oct-2015) (Revised by SO, 9-Jul-2018)

Ref Expression
Hypotheses mdetfval.d 
|- D = ( N maDet R )
mdetfval.a 
|- A = ( N Mat R )
mdetfval.b 
|- B = ( Base ` A )
mdetfval.p 
|- P = ( Base ` ( SymGrp ` N ) )
mdetfval.y 
|- Y = ( ZRHom ` R )
mdetfval.s 
|- S = ( pmSgn ` N )
mdetfval.t 
|- .x. = ( .r ` R )
mdetfval.u 
|- U = ( mulGrp ` R )
Assertion mdetleib 
|- ( M e. B -> ( D ` M ) = ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetfval.d 
 |-  D = ( N maDet R )
2 mdetfval.a 
 |-  A = ( N Mat R )
3 mdetfval.b 
 |-  B = ( Base ` A )
4 mdetfval.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
5 mdetfval.y 
 |-  Y = ( ZRHom ` R )
6 mdetfval.s 
 |-  S = ( pmSgn ` N )
7 mdetfval.t 
 |-  .x. = ( .r ` R )
8 mdetfval.u 
 |-  U = ( mulGrp ` R )
9 oveq 
 |-  ( m = M -> ( ( p ` x ) m x ) = ( ( p ` x ) M x ) )
10 9 mpteq2dv 
 |-  ( m = M -> ( x e. N |-> ( ( p ` x ) m x ) ) = ( x e. N |-> ( ( p ` x ) M x ) ) )
11 10 oveq2d 
 |-  ( m = M -> ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) = ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) )
12 11 oveq2d 
 |-  ( m = M -> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) = ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) )
13 12 mpteq2dv 
 |-  ( m = M -> ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) = ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) )
14 13 oveq2d 
 |-  ( m = M -> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) = ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) )
15 1 2 3 4 5 6 7 8 mdetfval 
 |-  D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) )
16 ovex 
 |-  ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) e. _V
17 14 15 16 fvmpt 
 |-  ( M e. B -> ( D ` M ) = ( R gsum ( p e. P |-> ( ( ( Y o. S ) ` p ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) )