Definition df-marepv

Description: Function replacing a column of a matrix by a vector. (Contributed by AV, 9-Feb-2019) (Revised by AV, 26-Feb-2019)

	Ref	Expression
Assertion	df-marepv	⊢ matRepV = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑟 ) ↑m 𝑛 ) ↦ ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmatrepV	⊢ matRepV
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		vv	⊢ 𝑣
12	8 5	cfv	⊢ ( Base ‘ 𝑟 )
13		cmap	⊢ ↑m
14	12 6 13	co	⊢ ( ( Base ‘ 𝑟 ) ↑m 𝑛 )
15		vk	⊢ 𝑘
16		vi	⊢ 𝑖
17		vj	⊢ 𝑗
18	17	cv	⊢ 𝑗
19	15	cv	⊢ 𝑘
20	18 19	wceq	⊢ 𝑗 = 𝑘
21	11	cv	⊢ 𝑣
22	16	cv	⊢ 𝑖
23	22 21	cfv	⊢ ( 𝑣 ‘ 𝑖 )
24	4	cv	⊢ 𝑚
25	22 18 24	co	⊢ ( 𝑖 𝑚 𝑗 )
26	20 23 25	cif	⊢ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) )
27	16 17 6 6 26	cmpo	⊢ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) )
28	15 6 27	cmpt	⊢ ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) )
29	4 11 10 14 28	cmpo	⊢ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑟 ) ↑m 𝑛 ) ↦ ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
30	1 3 2 2 29	cmpo	⊢ ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑟 ) ↑m 𝑛 ) ↦ ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
31	0 30	wceq	⊢ matRepV = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) , 𝑣 ∈ ( ( Base ‘ 𝑟 ) ↑m 𝑛 ) ↦ ( 𝑘 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )