Theorem maduval

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

	Ref	Expression
Hypotheses	madufval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	madufval.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	madufval.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
	madufval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	madufval.o	⊢ 1 = ( 1r ‘ 𝑅 )
	madufval.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	maduval	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐽 ‘ 𝑀 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		madufval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		madufval.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
3		madufval.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
4		madufval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
5		madufval.o	⊢ 1 = ( 1r ‘ 𝑅 )
6		madufval.z	⊢ 0 = ( 0g ‘ 𝑅 )
7	1 4	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
8	7	simpld	⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
9		mpoexga	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) ∈ V )
10	8 8 9	syl2anc	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) ∈ V )
11		oveq	⊢ ( 𝑚 = 𝑀 → ( 𝑘 𝑚 𝑙 ) = ( 𝑘 𝑀 𝑙 ) )
12	11	ifeq2d	⊢ ( 𝑚 = 𝑀 → if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) = if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) )
13	12	mpoeq3dv	⊢ ( 𝑚 = 𝑀 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) )
14	13	3ad2ant1	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) )
15	14	fveq2d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) = ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) )
16	15	mpoeq3dva	⊢ ( 𝑚 = 𝑀 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) )
17	1 2 3 4 5 6	madufval	⊢ 𝐽 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑚 𝑙 ) ) ) ) ) )
18	16 17	fvmptg	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) ∈ V ) → ( 𝐽 ‘ 𝑀 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) )
19	10 18	mpdan	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐽 ‘ 𝑀 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) )