# 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 ) )