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 
|- A = ( N Mat R )
minmar1marrep.b 
|- B = ( Base ` A )
minmar1marrep.o 
|- .1. = ( 1r ` R )
Assertion minmar1marrep 
|- ( ( R e. Ring /\ M e. B ) -> ( ( N minMatR1 R ) ` M ) = ( M ( N matRRep R ) .1. ) )

Proof

Step Hyp Ref Expression
1 minmar1marrep.a 
 |-  A = ( N Mat R )
2 minmar1marrep.b 
 |-  B = ( Base ` A )
3 minmar1marrep.o 
 |-  .1. = ( 1r ` R )
4 eqid 
 |-  ( N minMatR1 R ) = ( N minMatR1 R )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 1 2 4 3 5 minmar1val0 
 |-  ( M e. B -> ( ( N minMatR1 R ) ` M ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , ( 0g ` R ) ) , ( i M j ) ) ) ) )
7 6 adantl 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( N minMatR1 R ) ` M ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , ( 0g ` R ) ) , ( i M j ) ) ) ) )
8 simpr 
 |-  ( ( R e. Ring /\ M e. B ) -> M e. B )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 9 3 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
11 10 adantr 
 |-  ( ( R e. Ring /\ M e. B ) -> .1. e. ( Base ` R ) )
12 eqid 
 |-  ( N matRRep R ) = ( N matRRep R )
13 1 2 12 5 marrepval0 
 |-  ( ( M e. B /\ .1. e. ( Base ` R ) ) -> ( M ( N matRRep R ) .1. ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , ( 0g ` R ) ) , ( i M j ) ) ) ) )
14 8 11 13 syl2anc 
 |-  ( ( R e. Ring /\ M e. B ) -> ( M ( N matRRep R ) .1. ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , ( 0g ` R ) ) , ( i M j ) ) ) ) )
15 7 14 eqtr4d 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( N minMatR1 R ) ` M ) = ( M ( N matRRep R ) .1. ) )