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

Metamath Proof Explorer

Theorem maducoevalmin1

Description: The coefficients of an adjunct (matrix of cofactors) expressed as determinants of the minor matrices (alternative definition) of the original matrix. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses maducoevalmin1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
maducoevalmin1.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
maducoevalmin1.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
maducoevalmin1.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
Assertion maducoevalmin1 ( ( 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁 ) → ( 𝐼 ( 𝐽 ‘ 𝑀 ) 𝐻 ) = ( 𝐷 ‘ ( 𝐻 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 maducoevalmin1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 maducoevalmin1.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 maducoevalmin1.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
4 maducoevalmin1.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 1 3 4 2 5 6 maducoeval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁 ) → ( 𝐼 ( 𝐽 ‘ 𝑀 ) 𝐻 ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐻 , if ( 𝑗 = 𝐼 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
8 eqid ⊢ ( 𝑁 minMatR1 𝑅 ) = ( 𝑁 minMatR1 𝑅 )
9 1 2 8 5 6 minmar1val ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ) → ( 𝐻 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐻 , if ( 𝑗 = 𝐼 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
10 9 3com23 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁 ) → ( 𝐻 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐼 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐻 , if ( 𝑗 = 𝐼 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
11 10 eqcomd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐻 , if ( 𝑗 = 𝐼 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝐻 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐼 ) )
12 11 fveq2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐻 , if ( 𝑗 = 𝐼 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) = ( 𝐷 ‘ ( 𝐻 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐼 ) ) )
13 7 12 eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁 ) → ( 𝐼 ( 𝐽 ‘ 𝑀 ) 𝐻 ) = ( 𝐷 ‘ ( 𝐻 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐼 ) ) )