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

Metamath Proof Explorer

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 ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )