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 ⊢ 𝐴 = ( 𝑁 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 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) )