This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdetleib1

Description: Full substitution of an alternative determinant definition (also known as Leibniz' Formula). (Contributed by Stefan O'Rear, 3-Oct-2015) (Revised by AV, 26-Dec-2018)

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

Proof

Step Hyp Ref Expression
1 mdetfval1.d 
 |-  D = ( N maDet R )
2 mdetfval1.a 
 |-  A = ( N Mat R )
3 mdetfval1.b 
 |-  B = ( Base ` A )
4 mdetfval1.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
5 mdetfval1.y 
 |-  Y = ( ZRHom ` R )
6 mdetfval1.s 
 |-  S = ( pmSgn ` N )
7 mdetfval1.t 
 |-  .x. = ( .r ` R )
8 mdetfval1.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 ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) = ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) )
13 12 mpteq2dv 
 |-  ( m = M -> ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) = ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) )
14 13 oveq2d 
 |-  ( m = M -> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) = ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) )
15 1 2 3 4 5 6 7 8 mdetfval1 
 |-  D = ( m e. B |-> ( R gsum ( p e. P |-> ( ( Y ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) m x ) ) ) ) ) ) )
16 ovex 
 |-  ( R gsum ( p e. P |-> ( ( Y ` ( 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 ` ( S ` p ) ) .x. ( U gsum ( x e. N |-> ( ( p ` x ) M x ) ) ) ) ) ) )