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

Metamath Proof Explorer

Theorem ma1repvcl

Description: Closure of the column replacement function for identity matrices. (Contributed by AV, 15-Feb-2019) (Revised by AV, 26-Feb-2019)

Ref Expression
Hypotheses marepvcl.a 
|- A = ( N Mat R )
marepvcl.b 
|- B = ( Base ` A )
marepvcl.v 
|- V = ( ( Base ` R ) ^m N )
ma1repvcl.1 
|- .1. = ( 1r ` A )
Assertion ma1repvcl 
|- ( ( ( R e. Ring /\ N e. Fin ) /\ ( C e. V /\ K e. N ) ) -> ( ( .1. ( N matRepV R ) C ) ` K ) e. B )

Proof

Step Hyp Ref Expression
1 marepvcl.a 
 |-  A = ( N Mat R )
2 marepvcl.b 
 |-  B = ( Base ` A )
3 marepvcl.v 
 |-  V = ( ( Base ` R ) ^m N )
4 ma1repvcl.1 
 |-  .1. = ( 1r ` A )
5 simpll 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( C e. V /\ K e. N ) ) -> R e. Ring )
6 1 fveq2i 
 |-  ( 1r ` A ) = ( 1r ` ( N Mat R ) )
7 4 6 eqtri 
 |-  .1. = ( 1r ` ( N Mat R ) )
8 1 2 7 mat1bas 
 |-  ( ( R e. Ring /\ N e. Fin ) -> .1. e. B )
9 8 anim1i 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( C e. V /\ K e. N ) ) -> ( .1. e. B /\ ( C e. V /\ K e. N ) ) )
10 3anass 
 |-  ( ( .1. e. B /\ C e. V /\ K e. N ) <-> ( .1. e. B /\ ( C e. V /\ K e. N ) ) )
11 9 10 sylibr 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( C e. V /\ K e. N ) ) -> ( .1. e. B /\ C e. V /\ K e. N ) )
12 1 2 3 marepvcl 
 |-  ( ( R e. Ring /\ ( .1. e. B /\ C e. V /\ K e. N ) ) -> ( ( .1. ( N matRepV R ) C ) ` K ) e. B )
13 5 11 12 syl2anc 
 |-  ( ( ( R e. Ring /\ N e. Fin ) /\ ( C e. V /\ K e. N ) ) -> ( ( .1. ( N matRepV R ) C ) ` K ) e. B )