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

Metamath Proof Explorer

Theorem maduval

Description: Second substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

		Ref	Expression
	Hypotheses	madufval.a	\|- A = ( N Mat R )
		madufval.d	\|- D = ( N maDet R )
		madufval.j	\|- J = ( N maAdju R )
		madufval.b	\|- B = ( Base ` A )
		madufval.o	\|- .1. = ( 1r ` R )
		madufval.z	\|- .0. = ( 0g ` R )
	Assertion	maduval	\|- ( M e. B -> ( J ` M ) = ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		madufval.a	\|- A = ( N Mat R )
2		madufval.d	\|- D = ( N maDet R )
3		madufval.j	\|- J = ( N maAdju R )
4		madufval.b	\|- B = ( Base ` A )
5		madufval.o	\|- .1. = ( 1r ` R )
6		madufval.z	\|- .0. = ( 0g ` R )
7	1 4	matrcl	\|- ( M e. B -> ( N e. Fin /\ R e. _V ) )
8	7	simpld	\|- ( M e. B -> N e. Fin )
9		mpoexga	\|- ( ( N e. Fin /\ N e. Fin ) -> ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) e. _V )
10	8 8 9	syl2anc	\|- ( M e. B -> ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) e. _V )
11		oveq	\|- ( m = M -> ( k m l ) = ( k M l ) )
12	11	ifeq2d	\|- ( m = M -> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) = if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) )
13	12	mpoeq3dv	\|- ( m = M -> ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) = ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) )
14	13	3ad2ant1	\|- ( ( m = M /\ i e. N /\ j e. N ) -> ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) = ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) )
15	14	fveq2d	\|- ( ( m = M /\ i e. N /\ j e. N ) -> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) = ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) )
16	15	mpoeq3dva	\|- ( m = M -> ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) ) = ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )
17	1 2 3 4 5 6	madufval	\|- J = ( m e. B \|-> ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) ) )
18	16 17	fvmptg	\|- ( ( M e. B /\ ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) e. _V ) -> ( J ` M ) = ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )
19	10 18	mpdan	\|- ( M e. B -> ( J ` M ) = ( i e. N , j e. N \|-> ( D ` ( k e. N , l e. N \|-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )