Theorem maducoeval

Description: An entry of 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	maducoeval	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , 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 2 3 4 5 6	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 ) ) ) ) ) )
8	7	3ad2ant1	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( 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 ) ) ) ) ) )
9		simp1r	|- ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> j = H )
10	9	eqeq2d	|- ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> ( k = j <-> k = H ) )
11		simp1l	|- ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> i = I )
12	11	eqeq2d	|- ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> ( l = i <-> l = I ) )
13	12	ifbid	|- ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> if ( l = i , .1. , .0. ) = if ( l = I , .1. , .0. ) )
14	10 13	ifbieq1d	|- ( ( ( i = I /\ j = H ) /\ k e. N /\ l e. N ) -> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) = if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) )
15	14	mpoeq3dva	|- ( ( i = I /\ j = H ) -> ( 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 = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) )
16	15	fveq2d	|- ( ( i = I /\ j = H ) -> ( 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 = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )
17	16	adantl	|- ( ( ( M e. B /\ I e. N /\ H e. N ) /\ ( i = I /\ j = H ) ) -> ( 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 = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )
18		simp2	|- ( ( M e. B /\ I e. N /\ H e. N ) -> I e. N )
19		simp3	|- ( ( M e. B /\ I e. N /\ H e. N ) -> H e. N )
20		fvexd	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) e. _V )
21	8 17 18 19 20	ovmpod	|- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )