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	$$⊢\mathrm{matRepV}=\left(n\in \mathrm{V},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)},v\in \left({{\mathrm{Base}}_r}^n\right)⟼\left(k\in n⟼\left(i\in n,j\in n⟼if\left(j=k,v\left(i\right),imj\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmatrepV	$$class\mathrm{matRepV}$$
1		vn	$$setvarn$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vm	$$setvarm$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvarn$$
7		cmat	$$class\mathrm{Mat}$$
8	3	cv	$$setvarr$$
9	6 8 7	co	$$class\left(n\mathrm{Mat}r\right)$$
10	9 5	cfv	$$class{\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}$$
11		vv	$$setvarv$$
12	8 5	cfv	$$class{\mathrm{Base}}_r$$
13		cmap	$$class{\uparrow }_{𝑚}$$
14	12 6 13	co	$$class\left({{\mathrm{Base}}_r}^n\right)$$
15		vk	$$setvark$$
16		vi	$$setvari$$
17		vj	$$setvarj$$
18	17	cv	$$setvarj$$
19	15	cv	$$setvark$$
20	18 19	wceq	$$wffj=k$$
21	11	cv	$$setvarv$$
22	16	cv	$$setvari$$
23	22 21	cfv	$$classv\left(i\right)$$
24	4	cv	$$setvarm$$
25	22 18 24	co	$$class\left(imj\right)$$
26	20 23 25	cif	$$classif\left(j=k,v\left(i\right),imj\right)$$
27	16 17 6 6 26	cmpo	$$class\left(i\in n,j\in n⟼if\left(j=k,v\left(i\right),imj\right)\right)$$
28	15 6 27	cmpt	$$class\left(k\in n⟼\left(i\in n,j\in n⟼if\left(j=k,v\left(i\right),imj\right)\right)\right)$$
29	4 11 10 14 28	cmpo	$$class\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)},v\in \left({{\mathrm{Base}}_r}^n\right)⟼\left(k\in n⟼\left(i\in n,j\in n⟼if\left(j=k,v\left(i\right),imj\right)\right)\right)\right)$$
30	1 3 2 2 29	cmpo	$$class\left(n\in \mathrm{V},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)},v\in \left({{\mathrm{Base}}_r}^n\right)⟼\left(k\in n⟼\left(i\in n,j\in n⟼if\left(j=k,v\left(i\right),imj\right)\right)\right)\right)\right)$$
31	0 30	wceq	$$wff\mathrm{matRepV}=\left(n\in \mathrm{V},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)},v\in \left({{\mathrm{Base}}_r}^n\right)⟼\left(k\in n⟼\left(i\in n,j\in n⟼if\left(j=k,v\left(i\right),imj\right)\right)\right)\right)\right)$$