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 = r ∈ V , o ∈ V ⟼ ⦋ 1 st ⁡ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ 1 st ⁡ o / n⦌ ⦋ 2 nd ⁡ o / p⦌ x ∈ Base r m × n , y ∈ Base r n × p ⟼ i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmmul class maMul
1 vr setvar r
2 cvv class V
3 vo setvar o
4 c1st class 1 st
5 3 cv setvar o
6 5 4 cfv class 1 st ⁡ o
7 6 4 cfv class 1 st ⁡ 1 st ⁡ o
8 vm setvar m
9 c2nd class 2 nd
10 6 9 cfv class 2 nd ⁡ 1 st ⁡ o
11 vn setvar n
12 5 9 cfv class 2 nd ⁡ o
13 vp setvar p
14 vx setvar x
15 cbs class Base
16 1 cv setvar r
17 16 15 cfv class Base r
18 cmap class ↑ 𝑚
19 8 cv setvar m
20 11 cv setvar n
21 19 20 cxp class m × n
22 17 21 18 co class Base r m × n
23 vy setvar y
24 13 cv setvar p
25 20 24 cxp class n × p
26 17 25 18 co class Base r n × p
27 vi setvar i
28 vk setvar k
29 cgsu class Σ𝑔
30 vj setvar j
31 27 cv setvar i
32 14 cv setvar x
33 30 cv setvar j
34 31 33 32 co class i x j
35 cmulr class ⋅ 𝑟
36 16 35 cfv class ⋅ r
37 23 cv setvar y
38 28 cv setvar k
39 33 38 37 co class j y k
40 34 39 36 co class i x j ⋅ r j y k
41 30 20 40 cmpt class j ∈ n ⟼ i x j ⋅ r j y k
42 16 41 29 co class ∑ r j ∈ n i x j ⋅ r j y k
43 27 28 19 24 42 cmpo class i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k
44 14 23 22 26 43 cmpo class x ∈ Base r m × n , y ∈ Base r n × p ⟼ i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k
45 13 12 44 csb class ⦋ 2 nd ⁡ o / p⦌ x ∈ Base r m × n , y ∈ Base r n × p ⟼ i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k
46 11 10 45 csb class ⦋ 2 nd ⁡ 1 st ⁡ o / n⦌ ⦋ 2 nd ⁡ o / p⦌ x ∈ Base r m × n , y ∈ Base r n × p ⟼ i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k
47 8 7 46 csb class ⦋ 1 st ⁡ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ 1 st ⁡ o / n⦌ ⦋ 2 nd ⁡ o / p⦌ x ∈ Base r m × n , y ∈ Base r n × p ⟼ i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k
48 1 3 2 2 47 cmpo class r ∈ V , o ∈ V ⟼ ⦋ 1 st ⁡ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ 1 st ⁡ o / n⦌ ⦋ 2 nd ⁡ o / p⦌ x ∈ Base r m × n , y ∈ Base r n × p ⟼ i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k
49 0 48 wceq wff maMul = r ∈ V , o ∈ V ⟼ ⦋ 1 st ⁡ 1 st ⁡ o / m⦌ ⦋ 2 nd ⁡ 1 st ⁡ o / n⦌ ⦋ 2 nd ⁡ o / p⦌ x ∈ Base r m × n , y ∈ Base r n × p ⟼ i ∈ m , k ∈ p ⟼ ∑ r j ∈ n i x j ⋅ r j y k