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=NMatR
marep01ma.b B=BaseA
marep01ma.r RCRing
marep01ma.0 0˙=0R
marep01ma.1 1˙=1R
Assertion marep01ma MBkN,lNifk=Hifl=I1˙0˙kMlB

Proof

Step Hyp Ref Expression
1 marep01ma.a A=NMatR
2 marep01ma.b B=BaseA
3 marep01ma.r RCRing
4 marep01ma.0 0˙=0R
5 marep01ma.1 1˙=1R
6 eqid BaseR=BaseR
7 1 2 matrcl MBNFinRV
8 7 simpld MBNFin
9 3 a1i MBRCRing
10 crngring RCRingRRing
11 6 5 ringidcl RRing1˙BaseR
12 3 10 11 mp2b 1˙BaseR
13 6 4 ring0cl RRing0˙BaseR
14 3 10 13 mp2b 0˙BaseR
15 12 14 ifcli ifl=I1˙0˙BaseR
16 15 a1i MBkNlNifl=I1˙0˙BaseR
17 simp2 MBkNlNkN
18 simp3 MBkNlNlN
19 id MBMB
20 19 2 eleqtrdi MBMBaseA
21 20 3ad2ant1 MBkNlNMBaseA
22 1 6 matecl kNlNMBaseAkMlBaseR
23 17 18 21 22 syl3anc MBkNlNkMlBaseR
24 16 23 ifcld MBkNlNifk=Hifl=I1˙0˙kMlBaseR
25 1 6 2 8 9 24 matbas2d MBkN,lNifk=Hifl=I1˙0˙kMlB