Metamath Proof Explorer


Theorem marepvcl

Description: Closure of the column replacement function for square matrices. (Contributed by AV, 14-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 )
Assertion marepvcl
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( ( M ( 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 eqid
 |-  ( N matRepV R ) = ( N matRepV R )
5 1 2 4 3 marepvval
 |-  ( ( M e. B /\ C e. V /\ K e. N ) -> ( ( M ( N matRepV R ) C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) )
6 5 adantl
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( ( M ( N matRepV R ) C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) )
7 eqid
 |-  ( Base ` R ) = ( Base ` R )
8 1 2 matrcl
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
9 8 simpld
 |-  ( M e. B -> N e. Fin )
10 9 3ad2ant1
 |-  ( ( M e. B /\ C e. V /\ K e. N ) -> N e. Fin )
11 10 adantl
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> N e. Fin )
12 simpl
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> R e. Ring )
13 elmapi
 |-  ( C e. ( ( Base ` R ) ^m N ) -> C : N --> ( Base ` R ) )
14 ffvelrn
 |-  ( ( C : N --> ( Base ` R ) /\ i e. N ) -> ( C ` i ) e. ( Base ` R ) )
15 14 ex
 |-  ( C : N --> ( Base ` R ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) )
16 13 15 syl
 |-  ( C e. ( ( Base ` R ) ^m N ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) )
17 16 3 eleq2s
 |-  ( C e. V -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) )
18 17 3ad2ant2
 |-  ( ( M e. B /\ C e. V /\ K e. N ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) )
19 18 adantl
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) )
20 19 imp
 |-  ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N ) -> ( C ` i ) e. ( Base ` R ) )
21 20 3adant3
 |-  ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> ( C ` i ) e. ( Base ` R ) )
22 simp2
 |-  ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> i e. N )
23 simp3
 |-  ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> j e. N )
24 2 eleq2i
 |-  ( M e. B <-> M e. ( Base ` A ) )
25 24 biimpi
 |-  ( M e. B -> M e. ( Base ` A ) )
26 25 3ad2ant1
 |-  ( ( M e. B /\ C e. V /\ K e. N ) -> M e. ( Base ` A ) )
27 26 adantl
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> M e. ( Base ` A ) )
28 27 3ad2ant1
 |-  ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> M e. ( Base ` A ) )
29 1 7 matecl
 |-  ( ( i e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( i M j ) e. ( Base ` R ) )
30 22 23 28 29 syl3anc
 |-  ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` R ) )
31 21 30 ifcld
 |-  ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> if ( j = K , ( C ` i ) , ( i M j ) ) e. ( Base ` R ) )
32 1 7 2 11 12 31 matbas2d
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) e. B )
33 6 32 eqeltrd
 |-  ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( ( M ( N matRepV R ) C ) ` K ) e. B )