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

Definition df-marrep 18632
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
Distinct variable group:   , , , , , , ,

Detailed syntax breakdown of Definition df-marrep
StepHypRef Expression
1 cmarrep 18630 . 2
2 vn . . 3
3 vr . . 3
4 cvv 3081 . . 3
5 vm . . . 4
6 vs . . . 4
72cv 1369 . . . . . 6
83cv 1369 . . . . . 6
9 cmat 18496 . . . . . 6
107, 8, 9co 6222 . . . . 5
11 cbs 14332 . . . . 5
1210, 11cfv 5537 . . . 4
138, 11cfv 5537 . . . 4
14 vk . . . . 5
15 vl . . . . 5
16 vi . . . . . 6
17 vj . . . . . 6
1816, 14weq 1696 . . . . . . 7
1917, 15weq 1696 . . . . . . . 8
206cv 1369 . . . . . . . 8
21 c0g 14537 . . . . . . . . 9
228, 21cfv 5537 . . . . . . . 8
2319, 20, 22cif 3905 . . . . . . 7
2416cv 1369 . . . . . . . 8
2517cv 1369 . . . . . . . 8
265cv 1369 . . . . . . . 8
2724, 25, 26co 6222 . . . . . . 7
2818, 23, 27cif 3905 . . . . . 6
2916, 17, 7, 7, 28cmpt2 6224 . . . . 5
3014, 15, 7, 7, 29cmpt2 6224 . . . 4
315, 6, 12, 13, 30cmpt2 6224 . . 3
322, 3, 4, 4, 31cmpt2 6224 . 2
331, 32wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  marrepfval  18634
  Copyright terms: Public domain W3C validator