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 ) ) )
5 4 adantr 
 |-  ( ( ( 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 ) )
11 10 adantr 
 |-  ( ( R e. Ring /\ M e. B ) -> ( 1r ` R ) e. ( Base ` R ) )
12 7 8 11 3jca 
 |-  ( ( R e. Ring /\ M e. B ) -> ( R e. Ring /\ M e. B /\ ( 1r ` R ) e. ( Base ` R ) ) )
13 1 2 marrepcl 
 |-  ( ( ( 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 )
14 12 13 sylan 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) ( 1r ` R ) ) L ) e. B )
15 6 14 eqeltrd 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( K ( ( N minMatR1 R ) ` M ) L ) e. B )