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

Detailed syntax breakdown

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