# Metamath Proof Explorer

Description: An entry of the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
Hypotheses madufval.a 𝐴 = ( 𝑁 Mat 𝑅 )
madufval.b 𝐵 = ( Base ‘ 𝐴 )
madufval.o 1 = ( 1r𝑅 )
madufval.z 0 = ( 0g𝑅 )
Assertion maducoeval ( ( 𝑀𝐵𝐼𝑁𝐻𝑁 ) → ( 𝐼 ( 𝐽𝑀 ) 𝐻 ) = ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 madufval.a 𝐴 = ( 𝑁 Mat 𝑅 )
4 madufval.b 𝐵 = ( Base ‘ 𝐴 )
5 madufval.o 1 = ( 1r𝑅 )
6 madufval.z 0 = ( 0g𝑅 )
7 1 2 3 4 5 6 maduval ( 𝑀𝐵 → ( 𝐽𝑀 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) )
8 7 3ad2ant1 ( ( 𝑀𝐵𝐼𝑁𝐻𝑁 ) → ( 𝐽𝑀 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ) )
9 simp1r ( ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) ∧ 𝑘𝑁𝑙𝑁 ) → 𝑗 = 𝐻 )
10 9 eqeq2d ( ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) ∧ 𝑘𝑁𝑙𝑁 ) → ( 𝑘 = 𝑗𝑘 = 𝐻 ) )
11 simp1l ( ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) ∧ 𝑘𝑁𝑙𝑁 ) → 𝑖 = 𝐼 )
12 11 eqeq2d ( ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) ∧ 𝑘𝑁𝑙𝑁 ) → ( 𝑙 = 𝑖𝑙 = 𝐼 ) )
13 12 ifbid ( ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) ∧ 𝑘𝑁𝑙𝑁 ) → if ( 𝑙 = 𝑖 , 1 , 0 ) = if ( 𝑙 = 𝐼 , 1 , 0 ) )
14 10 13 ifbieq1d ( ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) ∧ 𝑘𝑁𝑙𝑁 ) → if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) = if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) )
15 14 mpoeq3dva ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) → ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) = ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) )
16 15 fveq2d ( ( 𝑖 = 𝐼𝑗 = 𝐻 ) → ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) = ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) )
17 16 adantl ( ( ( 𝑀𝐵𝐼𝑁𝐻𝑁 ) ∧ ( 𝑖 = 𝐼𝑗 = 𝐻 ) ) → ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝑗 , if ( 𝑙 = 𝑖 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) = ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) )
18 simp2 ( ( 𝑀𝐵𝐼𝑁𝐻𝑁 ) → 𝐼𝑁 )
19 simp3 ( ( 𝑀𝐵𝐼𝑁𝐻𝑁 ) → 𝐻𝑁 )
20 fvexd ( ( 𝑀𝐵𝐼𝑁𝐻𝑁 ) → ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) ∈ V )
21 8 17 18 19 20 ovmpod ( ( 𝑀𝐵𝐼𝑁𝐻𝑁 ) → ( 𝐼 ( 𝐽𝑀 ) 𝐻 ) = ( 𝐷 ‘ ( 𝑘𝑁 , 𝑙𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) )