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 )