MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mamu Structured version   Visualization version   GIF version

Definition df-mamu 19947
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.)
Assertion
Ref Expression
df-mamu maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st ‘(1st𝑜)) / 𝑚(2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))))))
Distinct variable group:   𝑖,𝑗,𝑘,𝑚,𝑛,𝑜,𝑝,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-mamu
StepHypRef Expression
1 cmmul 19946 . 2 class maMul
2 vr . . 3 setvar 𝑟
3 vo . . 3 setvar 𝑜
4 cvv 3168 . . 3 class V
5 vm . . . 4 setvar 𝑚
63cv 1473 . . . . . 6 class 𝑜
7 c1st 7030 . . . . . 6 class 1st
86, 7cfv 5786 . . . . 5 class (1st𝑜)
98, 7cfv 5786 . . . 4 class (1st ‘(1st𝑜))
10 vn . . . . 5 setvar 𝑛
11 c2nd 7031 . . . . . 6 class 2nd
128, 11cfv 5786 . . . . 5 class (2nd ‘(1st𝑜))
13 vp . . . . . 6 setvar 𝑝
146, 11cfv 5786 . . . . . 6 class (2nd𝑜)
15 vx . . . . . . 7 setvar 𝑥
16 vy . . . . . . 7 setvar 𝑦
172cv 1473 . . . . . . . . 9 class 𝑟
18 cbs 15637 . . . . . . . . 9 class Base
1917, 18cfv 5786 . . . . . . . 8 class (Base‘𝑟)
205cv 1473 . . . . . . . . 9 class 𝑚
2110cv 1473 . . . . . . . . 9 class 𝑛
2220, 21cxp 5022 . . . . . . . 8 class (𝑚 × 𝑛)
23 cmap 7717 . . . . . . . 8 class 𝑚
2419, 22, 23co 6523 . . . . . . 7 class ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛))
2513cv 1473 . . . . . . . . 9 class 𝑝
2621, 25cxp 5022 . . . . . . . 8 class (𝑛 × 𝑝)
2719, 26, 23co 6523 . . . . . . 7 class ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝))
28 vi . . . . . . . 8 setvar 𝑖
29 vk . . . . . . . 8 setvar 𝑘
30 vj . . . . . . . . . 10 setvar 𝑗
3128cv 1473 . . . . . . . . . . . 12 class 𝑖
3230cv 1473 . . . . . . . . . . . 12 class 𝑗
3315cv 1473 . . . . . . . . . . . 12 class 𝑥
3431, 32, 33co 6523 . . . . . . . . . . 11 class (𝑖𝑥𝑗)
3529cv 1473 . . . . . . . . . . . 12 class 𝑘
3616cv 1473 . . . . . . . . . . . 12 class 𝑦
3732, 35, 36co 6523 . . . . . . . . . . 11 class (𝑗𝑦𝑘)
38 cmulr 15711 . . . . . . . . . . . 12 class .r
3917, 38cfv 5786 . . . . . . . . . . 11 class (.r𝑟)
4034, 37, 39co 6523 . . . . . . . . . 10 class ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))
4130, 21, 40cmpt 4633 . . . . . . . . 9 class (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))
42 cgsu 15866 . . . . . . . . 9 class Σg
4317, 41, 42co 6523 . . . . . . . 8 class (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))
4428, 29, 20, 25, 43cmpt2 6525 . . . . . . 7 class (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))))
4515, 16, 24, 27, 44cmpt2 6525 . . . . . 6 class (𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
4613, 14, 45csb 3494 . . . . 5 class (2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
4710, 12, 46csb 3494 . . . 4 class (2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
485, 9, 47csb 3494 . . 3 class (1st ‘(1st𝑜)) / 𝑚(2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
492, 3, 4, 4, 48cmpt2 6525 . 2 class (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st ‘(1st𝑜)) / 𝑚(2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))))))
501, 49wceq 1474 1 wff maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st ‘(1st𝑜)) / 𝑚(2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))))))
Colors of variables: wff setvar class
This definition is referenced by:  mamufval  19948
  Copyright terms: Public domain W3C validator