Metamath Proof Explorer


Theorem marep01ma

Description: Replacing a row of a square matrix by a row with 0's and a 1 results in a square matrix of the same dimension. (Contributed by AV, 30-Dec-2018)

Ref Expression
Hypotheses marep01ma.a
|- A = ( N Mat R )
marep01ma.b
|- B = ( Base ` A )
marep01ma.r
|- R e. CRing
marep01ma.0
|- .0. = ( 0g ` R )
marep01ma.1
|- .1. = ( 1r ` R )
Assertion marep01ma
|- ( M e. B -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) e. B )

Proof

Step Hyp Ref Expression
1 marep01ma.a
 |-  A = ( N Mat R )
2 marep01ma.b
 |-  B = ( Base ` A )
3 marep01ma.r
 |-  R e. CRing
4 marep01ma.0
 |-  .0. = ( 0g ` R )
5 marep01ma.1
 |-  .1. = ( 1r ` R )
6 eqid
 |-  ( Base ` R ) = ( Base ` R )
7 1 2 matrcl
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
8 7 simpld
 |-  ( M e. B -> N e. Fin )
9 3 a1i
 |-  ( M e. B -> R e. CRing )
10 crngring
 |-  ( R e. CRing -> R e. Ring )
11 6 5 ringidcl
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
12 3 10 11 mp2b
 |-  .1. e. ( Base ` R )
13 6 4 ring0cl
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
14 3 10 13 mp2b
 |-  .0. e. ( Base ` R )
15 12 14 ifcli
 |-  if ( l = I , .1. , .0. ) e. ( Base ` R )
16 15 a1i
 |-  ( ( M e. B /\ k e. N /\ l e. N ) -> if ( l = I , .1. , .0. ) e. ( Base ` R ) )
17 simp2
 |-  ( ( M e. B /\ k e. N /\ l e. N ) -> k e. N )
18 simp3
 |-  ( ( M e. B /\ k e. N /\ l e. N ) -> l e. N )
19 id
 |-  ( M e. B -> M e. B )
20 19 2 eleqtrdi
 |-  ( M e. B -> M e. ( Base ` A ) )
21 20 3ad2ant1
 |-  ( ( M e. B /\ k e. N /\ l e. N ) -> M e. ( Base ` A ) )
22 1 6 matecl
 |-  ( ( k e. N /\ l e. N /\ M e. ( Base ` A ) ) -> ( k M l ) e. ( Base ` R ) )
23 17 18 21 22 syl3anc
 |-  ( ( M e. B /\ k e. N /\ l e. N ) -> ( k M l ) e. ( Base ` R ) )
24 16 23 ifcld
 |-  ( ( M e. B /\ k e. N /\ l e. N ) -> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) e. ( Base ` R ) )
25 1 6 2 8 9 24 matbas2d
 |-  ( M e. B -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) e. B )