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 ) ) ) ) ) ) )