Definition df-marrep 22564

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 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))))))

Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙,𝑠

Detailed syntax breakdown of Definition df-marrep

Step	Hyp	Ref	Expression
1		cmarrep 22562	. 2 class matRRep
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3480	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6		vs	. . . 4 setvar 𝑠
7	2	cv 1539	. . . . . 6 class 𝑛
8	3	cv 1539	. . . . . 6 class 𝑟
9		cmat 22411	. . . . . 6 class Mat
10	7, 8, 9	co 7431	. . . . 5 class (𝑛 Mat 𝑟)
11		cbs 17247	. . . . 5 class Base
12	10, 11	cfv 6561	. . . 4 class (Base‘(𝑛 Mat 𝑟))
13	8, 11	cfv 6561	. . . 4 class (Base‘𝑟)
14		vk	. . . . 5 setvar 𝑘
15		vl	. . . . 5 setvar 𝑙
16		vi	. . . . . 6 setvar 𝑖
17		vj	. . . . . 6 setvar 𝑗
18	16, 14	weq 1962	. . . . . . 7 wff 𝑖 = 𝑘
19	17, 15	weq 1962	. . . . . . . 8 wff 𝑗 = 𝑙
20	6	cv 1539	. . . . . . . 8 class 𝑠
21		c0g 17484	. . . . . . . . 9 class 0g
22	8, 21	cfv 6561	. . . . . . . 8 class (0g‘𝑟)
23	19, 20, 22	cif 4525	. . . . . . 7 class if(𝑗 = 𝑙, 𝑠, (0g‘𝑟))
24	16	cv 1539	. . . . . . . 8 class 𝑖
25	17	cv 1539	. . . . . . . 8 class 𝑗
26	5	cv 1539	. . . . . . . 8 class 𝑚
27	24, 25, 26	co 7431	. . . . . . 7 class (𝑖𝑚𝑗)
28	18, 23, 27	cif 4525	. . . . . 6 class if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))
29	16, 17, 7, 7, 28	cmpo 7433	. . . . 5 class (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗)))
30	14, 15, 7, 7, 29	cmpo 7433	. . . 4 class (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))))
31	5, 6, 12, 13, 30	cmpo 7433	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗)))))
32	2, 3, 4, 4, 31	cmpo 7433	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))))))
33	1, 32	wceq 1540	1 wff matRRep = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))))))

This definition is referenced by:  marrepfval  22566