# Metamath Proof Explorer

## Theorem minmar1cl

Description: Closure of the row replacement function for square matrices: The matrix for a minor is a matrix. (Contributed by AV, 13-Feb-2019)

Ref Expression
Hypotheses minmar1cl.a
`|- A = ( N Mat R )`
minmar1cl.b
`|- B = ( Base ` A )`
Assertion minmar1cl
`|- ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( K ( ( N minMatR1 R ) ` M ) L ) e. B )`

### Proof

Step Hyp Ref Expression
1 minmar1cl.a
` |-  A = ( N Mat R )`
2 minmar1cl.b
` |-  B = ( Base ` A )`
3 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
4 1 2 3 minmar1marrep
` |-  ( ( R e. Ring /\ M e. B ) -> ( ( N minMatR1 R ) ` M ) = ( M ( N matRRep R ) ( 1r ` R ) ) )`
` |-  ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( ( N minMatR1 R ) ` M ) = ( M ( N matRRep R ) ( 1r ` R ) ) )`
6 5 oveqd
` |-  ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( K ( ( N minMatR1 R ) ` M ) L ) = ( K ( M ( N matRRep R ) ( 1r ` R ) ) L ) )`
7 simpl
` |-  ( ( R e. Ring /\ M e. B ) -> R e. Ring )`
8 simpr
` |-  ( ( R e. Ring /\ M e. B ) -> M e. B )`
9 eqid
` |-  ( Base ` R ) = ( Base ` R )`
10 9 3 ringidcl
` |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )`
` |-  ( ( R e. Ring /\ M e. B ) -> ( 1r ` R ) e. ( Base ` R ) )`
` |-  ( ( R e. Ring /\ M e. B ) -> ( R e. Ring /\ M e. B /\ ( 1r ` R ) e. ( Base ` R ) ) )`
` |-  ( ( ( R e. Ring /\ M e. B /\ ( 1r ` R ) e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) ( 1r ` R ) ) L ) e. B )`
` |-  ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) ( 1r ` R ) ) L ) e. B )`
` |-  ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( K ( ( N minMatR1 R ) ` M ) L ) e. B )`