Metamath Proof Explorer

Theorem minmar1val0

Description: Second substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

		Ref	Expression
	Hypotheses	minmar1fval.a	\|- A = ( N Mat R )
		minmar1fval.b	\|- B = ( Base ` A )
		minmar1fval.q	\|- Q = ( N minMatR1 R )
		minmar1fval.o	\|- .1. = ( 1r ` R )
		minmar1fval.z	\|- .0. = ( 0g ` R )
	Assertion	minmar1val0	\|- ( M e. B -> ( Q ` M ) = ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		minmar1fval.a	\|- A = ( N Mat R )
2		minmar1fval.b	\|- B = ( Base ` A )
3		minmar1fval.q	\|- Q = ( N minMatR1 R )
4		minmar1fval.o	\|- .1. = ( 1r ` R )
5		minmar1fval.z	\|- .0. = ( 0g ` R )
6	1 2	matrcl	\|- ( M e. B -> ( N e. Fin /\ R e. _V ) )
7	6	simpld	\|- ( M e. B -> N e. Fin )
8		mpoexga	\|- ( ( N e. Fin /\ N e. Fin ) -> ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) e. _V )
9	7 7 8	syl2anc	\|- ( M e. B -> ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) e. _V )
10		oveq	\|- ( m = M -> ( i m j ) = ( i M j ) )
11	10	ifeq2d	\|- ( m = M -> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) = if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) )
12	11	mpoeq3dv	\|- ( m = M -> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) = ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) )
13	12	mpoeq3dv	\|- ( m = M -> ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) = ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) )
14	1 2 3 4 5	minmar1fval	\|- Q = ( m e. B \|-> ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) )
15	13 14	fvmptg	\|- ( ( M e. B /\ ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) e. _V ) -> ( Q ` M ) = ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) )
16	9 15	mpdan	\|- ( M e. B -> ( Q ` M ) = ( k e. N , l e. N \|-> ( i e. N , j e. N \|-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) )