Metamath Proof Explorer

Theorem marrepcl

Description: Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019)

Ref Expression
Hypotheses marrepcl.a 
|- A = ( N Mat R )
marrepcl.b 
|- B = ( Base ` A )
Assertion marrepcl 
|- ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) S ) L ) e. B )

Proof

Step Hyp Ref Expression
1 marrepcl.a 
 |-  A = ( N Mat R )
2 marrepcl.b 
 |-  B = ( Base ` A )
3 eqid 
 |-  ( N matRRep R ) = ( N matRRep R )
4 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
5 1 2 3 4 marrepval 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) S ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , S , ( 0g ` R ) ) , ( i M j ) ) ) )
6 5 3adantl1 
 |-  ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) S ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , S , ( 0g ` R ) ) , ( 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 3ad2ant2 
 |-  ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) -> N e. Fin )
11 10 adantr 
 |-  ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> N e. Fin )
12 simpl1 
 |-  ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> R e. Ring )
13 simp3 
 |-  ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) -> S e. ( Base ` R ) )
14 7 4 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
15 14 3ad2ant1 
 |-  ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) -> ( 0g ` R ) e. ( Base ` R ) )
16 13 15 ifcld 
 |-  ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) -> if ( j = L , S , ( 0g ` R ) ) e. ( Base ` R ) )
17 16 adantr 
 |-  ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> if ( j = L , S , ( 0g ` R ) ) e. ( Base ` R ) )
18 17 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) /\ i e. N /\ j e. N ) -> if ( j = L , S , ( 0g ` R ) ) e. ( Base ` R ) )
19 simp2 
 |-  ( ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) /\ i e. N /\ j e. N ) -> i e. N )
20 simp3 
 |-  ( ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) /\ i e. N /\ j e. N ) -> j e. N )
21 2 eleq2i 
 |-  ( M e. B <-> M e. ( Base ` A ) )
22 21 biimpi 
 |-  ( M e. B -> M e. ( Base ` A ) )
23 22 3ad2ant2 
 |-  ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) -> M e. ( Base ` A ) )
24 23 adantr 
 |-  ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> M e. ( Base ` A ) )
25 24 3ad2ant1 
 |-  ( ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) /\ i e. N /\ j e. N ) -> M e. ( Base ` A ) )
26 1 7 matecl 
 |-  ( ( i e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( i M j ) e. ( Base ` R ) )
27 19 20 25 26 syl3anc 
 |-  ( ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` R ) )
28 18 27 ifcld 
 |-  ( ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) /\ i e. N /\ j e. N ) -> if ( i = K , if ( j = L , S , ( 0g ` R ) ) , ( i M j ) ) e. ( Base ` R ) )
29 1 7 2 11 12 28 matbas2d 
 |-  ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( i e. N , j e. N |-> if ( i = K , if ( j = L , S , ( 0g ` R ) ) , ( i M j ) ) ) e. B )
30 6 29 eqeltrd 
 |-  ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) S ) L ) e. B )