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 ffvelcdm 
 |-  ( ( 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 )