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

Metamath Proof Explorer

Theorem minmar1marrep

Description: The minor matrix is a special case of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019) (Revised by AV, 4-Jul-2022)

Ref Expression
Hypotheses minmar1marrep.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
minmar1marrep.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
minmar1marrep.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion minmar1marrep ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) )

Proof

Step Hyp Ref Expression
1 minmar1marrep.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 minmar1marrep.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 minmar1marrep.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 eqid ⊢ ( 𝑁 minMatR1 𝑅 ) = ( 𝑁 minMatR1 𝑅 )
5 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6 1 2 4 3 5 minmar1val0 ⊢ ( 𝑀 ∈ 𝐵 → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
7 6 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
8 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
11 10 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝑅 ) )
12 eqid ⊢ ( 𝑁 matRRep 𝑅 ) = ( 𝑁 matRRep 𝑅 )
13 1 2 12 5 marrepval0 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
14 8 11 13 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
15 7 14 eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) )