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

Definition df-mamu 20184
 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 20183 . 2 class maMul
2 vr . . 3 setvar 𝑟
3 vo . . 3 setvar 𝑜
4 cvv 3198 . . 3 class V
5 vm . . . 4 setvar 𝑚
63cv 1481 . . . . . 6 class 𝑜
7 c1st 7163 . . . . . 6 class 1st
86, 7cfv 5886 . . . . 5 class (1st𝑜)
98, 7cfv 5886 . . . 4 class (1st ‘(1st𝑜))
10 vn . . . . 5 setvar 𝑛
11 c2nd 7164 . . . . . 6 class 2nd
128, 11cfv 5886 . . . . 5 class (2nd ‘(1st𝑜))
13 vp . . . . . 6 setvar 𝑝
146, 11cfv 5886 . . . . . 6 class (2nd𝑜)
15 vx . . . . . . 7 setvar 𝑥
16 vy . . . . . . 7 setvar 𝑦
172cv 1481 . . . . . . . . 9 class 𝑟
18 cbs 15851 . . . . . . . . 9 class Base
1917, 18cfv 5886 . . . . . . . 8 class (Base‘𝑟)
205cv 1481 . . . . . . . . 9 class 𝑚
2110cv 1481 . . . . . . . . 9 class 𝑛
2220, 21cxp 5110 . . . . . . . 8 class (𝑚 × 𝑛)
23 cmap 7854 . . . . . . . 8 class 𝑚
2419, 22, 23co 6647 . . . . . . 7 class ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛))
2513cv 1481 . . . . . . . . 9 class 𝑝
2621, 25cxp 5110 . . . . . . . 8 class (𝑛 × 𝑝)
2719, 26, 23co 6647 . . . . . . 7 class ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝))
28 vi . . . . . . . 8 setvar 𝑖
29 vk . . . . . . . 8 setvar 𝑘
30 vj . . . . . . . . . 10 setvar 𝑗
3128cv 1481 . . . . . . . . . . . 12 class 𝑖
3230cv 1481 . . . . . . . . . . . 12 class 𝑗
3315cv 1481 . . . . . . . . . . . 12 class 𝑥
3431, 32, 33co 6647 . . . . . . . . . . 11 class (𝑖𝑥𝑗)
3529cv 1481 . . . . . . . . . . . 12 class 𝑘
3616cv 1481 . . . . . . . . . . . 12 class 𝑦
3732, 35, 36co 6647 . . . . . . . . . . 11 class (𝑗𝑦𝑘)
38 cmulr 15936 . . . . . . . . . . . 12 class .r
3917, 38cfv 5886 . . . . . . . . . . 11 class (.r𝑟)
4034, 37, 39co 6647 . . . . . . . . . 10 class ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))
4130, 21, 40cmpt 4727 . . . . . . . . 9 class (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))
42 cgsu 16095 . . . . . . . . 9 class Σg
4317, 41, 42co 6647 . . . . . . . 8 class (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))
4428, 29, 20, 25, 43cmpt2 6649 . . . . . . 7 class (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))))
4515, 16, 24, 27, 44cmpt2 6649 . . . . . 6 class (𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
4613, 14, 45csb 3531 . . . . 5 class (2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
4710, 12, 46csb 3531 . . . 4 class (2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
485, 9, 47csb 3531 . . 3 class (1st ‘(1st𝑜)) / 𝑚(2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘))))))
492, 3, 4, 4, 48cmpt2 6649 . 2 class (𝑟 ∈ V, 𝑜 ∈ V ↦ (1st ‘(1st𝑜)) / 𝑚(2nd ‘(1st𝑜)) / 𝑛(2nd𝑜) / 𝑝(𝑥 ∈ ((Base‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 (𝑛 × 𝑝)) ↦ (𝑖𝑚, 𝑘𝑝 ↦ (𝑟 Σg (𝑗𝑛 ↦ ((𝑖𝑥𝑗)(.r𝑟)(𝑗𝑦𝑘)))))))
501, 49wceq 1482 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  20185
 Copyright terms: Public domain W3C validator