Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-marrep Structured version   Unicode version

Definition df-marrep 19186
 Description: Define the matrices whose k-th row is replaced by 0's and an arbitrary element of the underlying ring at the l-th column. (Contributed by AV, 12-Feb-2019.)
Assertion
Ref Expression
df-marrep matRRep Mat
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-marrep
StepHypRef Expression
1 cmarrep 19184 . 2 matRRep
2 vn . . 3
3 vr . . 3
4 cvv 3109 . . 3
5 vm . . . 4
6 vs . . . 4
72cv 1394 . . . . . 6
83cv 1394 . . . . . 6
9 cmat 19035 . . . . . 6 Mat
107, 8, 9co 6296 . . . . 5 Mat
11 cbs 14643 . . . . 5
1210, 11cfv 5594 . . . 4 Mat
138, 11cfv 5594 . . . 4
14 vk . . . . 5
15 vl . . . . 5
16 vi . . . . . 6
17 vj . . . . . 6
1816, 14weq 1734 . . . . . . 7
1917, 15weq 1734 . . . . . . . 8
206cv 1394 . . . . . . . 8
21 c0g 14856 . . . . . . . . 9
228, 21cfv 5594 . . . . . . . 8
2319, 20, 22cif 3944 . . . . . . 7
2416cv 1394 . . . . . . . 8
2517cv 1394 . . . . . . . 8
265cv 1394 . . . . . . . 8
2724, 25, 26co 6296 . . . . . . 7
2818, 23, 27cif 3944 . . . . . 6
2916, 17, 7, 7, 28cmpt2 6298 . . . . 5
3014, 15, 7, 7, 29cmpt2 6298 . . . 4
315, 6, 12, 13, 30cmpt2 6298 . . 3 Mat
322, 3, 4, 4, 31cmpt2 6298 . 2 Mat
331, 32wceq 1395 1 matRRep Mat
 Colors of variables: wff setvar class This definition is referenced by:  marrepfval  19188
 Copyright terms: Public domain W3C validator