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

Metamath Proof Explorer

Definition df-mamu

Description: The operator which multiplies an m x n matrix with an n x p matrix, see also the definition in Lang p. 504. Note that it is not generally possible to recover the dimensions from the matrix, since all n x 0 and all 0 x n matrices are represented by the empty set. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Assertion df-mamu maMul = ( 𝑟 ∈ V , 𝑜 ∈ V ↦ ⦋ ( 1st ‘ ( 1st ‘ 𝑜 ) ) / 𝑚 ⦌ ⦋ ( 2nd ‘ ( 1st ‘ 𝑜 ) ) / 𝑛 ⦌ ⦋ ( 2nd ‘ 𝑜 ) / 𝑝 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmmul ⊢ maMul
1 vr ⊢ 𝑟
2 cvv ⊢ V
3 vo ⊢ 𝑜
4 c1st ⊢ 1st
5 3 cv ⊢ 𝑜
6 5 4 cfv ⊢ ( 1st ‘ 𝑜 )
7 6 4 cfv ⊢ ( 1st ‘ ( 1st ‘ 𝑜 ) )
8 vm ⊢ 𝑚
9 c2nd ⊢ 2nd
10 6 9 cfv ⊢ ( 2nd ‘ ( 1st ‘ 𝑜 ) )
11 vn ⊢ 𝑛
12 5 9 cfv ⊢ ( 2nd ‘ 𝑜 )
13 vp ⊢ 𝑝
14 vx ⊢ 𝑥
15 cbs ⊢ Base
16 1 cv ⊢ 𝑟
17 16 15 cfv ⊢ ( Base ‘ 𝑟 )
18 cmap ⊢ ↑m
19 8 cv ⊢ 𝑚
20 11 cv ⊢ 𝑛
21 19 20 cxp ⊢ ( 𝑚 × 𝑛 )
22 17 21 18 co ⊢ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) )
23 vy ⊢ 𝑦
24 13 cv ⊢ 𝑝
25 20 24 cxp ⊢ ( 𝑛 × 𝑝 )
26 17 25 18 co ⊢ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) )
27 vi ⊢ 𝑖
28 vk ⊢ 𝑘
29 cgsu ⊢ Σg
30 vj ⊢ 𝑗
31 27 cv ⊢ 𝑖
32 14 cv ⊢ 𝑥
33 30 cv ⊢ 𝑗
34 31 33 32 co ⊢ ( 𝑖 𝑥 𝑗 )
35 cmulr ⊢ .r
36 16 35 cfv ⊢ ( .r ‘ 𝑟 )
37 23 cv ⊢ 𝑦
38 28 cv ⊢ 𝑘
39 33 38 37 co ⊢ ( 𝑗 𝑦 𝑘 )
40 34 39 36 co ⊢ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) )
41 30 20 40 cmpt ⊢ ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) )
42 16 41 29 co ⊢ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) )
43 27 28 19 24 42 cmpo ⊢ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) )
44 14 23 22 26 43 cmpo ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) )
45 13 12 44 csb ⊢ ⦋ ( 2nd ‘ 𝑜 ) / 𝑝 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) )
46 11 10 45 csb ⊢ ⦋ ( 2nd ‘ ( 1st ‘ 𝑜 ) ) / 𝑛 ⦌ ⦋ ( 2nd ‘ 𝑜 ) / 𝑝 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) )
47 8 7 46 csb ⊢ ⦋ ( 1st ‘ ( 1st ‘ 𝑜 ) ) / 𝑚 ⦌ ⦋ ( 2nd ‘ ( 1st ‘ 𝑜 ) ) / 𝑛 ⦌ ⦋ ( 2nd ‘ 𝑜 ) / 𝑝 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) )
48 1 3 2 2 47 cmpo ⊢ ( 𝑟 ∈ V , 𝑜 ∈ V ↦ ⦋ ( 1st ‘ ( 1st ‘ 𝑜 ) ) / 𝑚 ⦌ ⦋ ( 2nd ‘ ( 1st ‘ 𝑜 ) ) / 𝑛 ⦌ ⦋ ( 2nd ‘ 𝑜 ) / 𝑝 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )
49 0 48 wceq ⊢ maMul = ( 𝑟 ∈ V , 𝑜 ∈ V ↦ ⦋ ( 1st ‘ ( 1st ‘ 𝑜 ) ) / 𝑚 ⦌ ⦋ ( 2nd ‘ ( 1st ‘ 𝑜 ) ) / 𝑛 ⦌ ⦋ ( 2nd ‘ 𝑜 ) / 𝑝 ⦌ ( 𝑥 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑚 × 𝑛 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑟 ) ↑m ( 𝑛 × 𝑝 ) ) ↦ ( 𝑖 ∈ 𝑚 , 𝑘 ∈ 𝑝 ↦ ( 𝑟 Σg ( 𝑗 ∈ 𝑛 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑟 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )