This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑗 = 𝑘 , ( 𝑣 ‘ 𝑖 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )