Metamath Proof Explorer

Definition df-marrep

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)

Ref Expression
Assertion df-marrep ⊢ matRRep = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r , s ∈ Base r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l s 0 r i m j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmarrep class matRRep
1 vn setvar n
2 cvv class V
3 vr setvar r
4 vm setvar m
5 cbs class Base
6 1 cv setvar n
7 cmat class Mat
8 3 cv setvar r
9 6 8 7 co class n Mat r
10 9 5 cfv class Base n Mat r
11 vs setvar s
12 8 5 cfv class Base r
13 vk setvar k
14 vl setvar l
15 vi setvar i
16 vj setvar j
17 15 cv setvar i
18 13 cv setvar k
19 17 18 wceq wff i = k
20 16 cv setvar j
21 14 cv setvar l
22 20 21 wceq wff j = l
23 11 cv setvar s
24 c0g class 0 𝑔
25 8 24 cfv class 0 r
26 22 23 25 cif class if j = l s 0 r
27 4 cv setvar m
28 17 20 27 co class i m j
29 19 26 28 cif class if i = k if j = l s 0 r i m j
30 15 16 6 6 29 cmpo class i ∈ n , j ∈ n ⟼ if i = k if j = l s 0 r i m j
31 13 14 6 6 30 cmpo class k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l s 0 r i m j
32 4 11 10 12 31 cmpo class m ∈ Base n Mat r , s ∈ Base r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l s 0 r i m j
33 1 3 2 2 32 cmpo class n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r , s ∈ Base r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l s 0 r i m j
34 0 33 wceq wff matRRep = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r , s ∈ Base r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l s 0 r i m j