Theorem mdetuni

Description: According to the definition in Weierstrass p. 272, the determinant function is the unique multilinear, alternating and normalized function from the algebra of square matrices of the same dimension over a commutative ring to this ring. So for any multilinear (mdetuni.li and mdetuni.sc), alternating (mdetuni.al) and normalized (mdetuni.no) function D (mdetuni.ff) from the algebra of square matrices (mdetuni.a) to their underlying commutative ring (mdetuni.cr), the function value of this function D for a matrix F (mdetuni.f) is the determinant of this matrix. (Contributed by Stefan O'Rear, 15-Jul-2018) (Revised by Alexander van der Vekens, 8-Feb-2019)

	Ref	Expression
Hypotheses	mdetuni.a	|- A = ( N Mat R )
	mdetuni.b	|- B = ( Base ` A )
	mdetuni.k	|- K = ( Base ` R )
	mdetuni.0g	|- .0. = ( 0g ` R )
	mdetuni.1r	|- .1. = ( 1r ` R )
	mdetuni.pg	|- .+ = ( +g ` R )
	mdetuni.tg	|- .x. = ( .r ` R )
	mdetuni.n	|- ( ph -> N e. Fin )
	mdetuni.r	|- ( ph -> R e. Ring )
	mdetuni.ff	|- ( ph -> D : B --> K )
	mdetuni.al	|- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
	mdetuni.li	|- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
	mdetuni.sc	|- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
	mdetuni.e	|- E = ( N maDet R )
	mdetuni.cr	|- ( ph -> R e. CRing )
	mdetuni.f	|- ( ph -> F e. B )
	mdetuni.no	|- ( ph -> ( D ` ( 1r ` A ) ) = .1. )
Assertion	mdetuni	|- ( ph -> ( D ` F ) = ( E ` F ) )

Proof

Step	Hyp	Ref	Expression
1		mdetuni.a	|- A = ( N Mat R )
2		mdetuni.b	|- B = ( Base ` A )
3		mdetuni.k	|- K = ( Base ` R )
4		mdetuni.0g	|- .0. = ( 0g ` R )
5		mdetuni.1r	|- .1. = ( 1r ` R )
6		mdetuni.pg	|- .+ = ( +g ` R )
7		mdetuni.tg	|- .x. = ( .r ` R )
8		mdetuni.n	|- ( ph -> N e. Fin )
9		mdetuni.r	|- ( ph -> R e. Ring )
10		mdetuni.ff	|- ( ph -> D : B --> K )
11		mdetuni.al	|- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
12		mdetuni.li	|- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
13		mdetuni.sc	|- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
14		mdetuni.e	|- E = ( N maDet R )
15		mdetuni.cr	|- ( ph -> R e. CRing )
16		mdetuni.f	|- ( ph -> F e. B )
17		mdetuni.no	|- ( ph -> ( D ` ( 1r ` A ) ) = .1. )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	mdetuni0	|- ( ph -> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )
19	17	oveq1d	|- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) = ( .1. .x. ( E ` F ) ) )
20	14 1 2 3	mdetcl	|- ( ( R e. CRing /\ F e. B ) -> ( E ` F ) e. K )
21	15 16 20	syl2anc	|- ( ph -> ( E ` F ) e. K )
22	3 7 5	ringlidm	|- ( ( R e. Ring /\ ( E ` F ) e. K ) -> ( .1. .x. ( E ` F ) ) = ( E ` F ) )
23	9 21 22	syl2anc	|- ( ph -> ( .1. .x. ( E ` F ) ) = ( E ` F ) )
24	18 19 23	3eqtrd	|- ( ph -> ( D ` F ) = ( E ` F ) )