| Step | Hyp | Ref
| Expression |
| 1 | | mvmulfval.x |
. 2
⊢ × =
(𝑅 maVecMul 〈𝑀, 𝑁〉) |
| 2 | | df-mvmul 22547 |
. . . 4
⊢ maVecMul
= (𝑟 ∈ V, 𝑜 ∈ V ↦
⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd
‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))) |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → maVecMul = (𝑟 ∈ V, 𝑜 ∈ V ↦
⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd
‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))))) |
| 4 | | fvex 6919 |
. . . . 5
⊢
(1st ‘𝑜) ∈ V |
| 5 | | fvex 6919 |
. . . . 5
⊢
(2nd ‘𝑜) ∈ V |
| 6 | | xpeq12 5710 |
. . . . . . 7
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → (𝑚 × 𝑛) = ((1st ‘𝑜) × (2nd
‘𝑜))) |
| 7 | 6 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → ((Base‘𝑟) ↑m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑m ((1st
‘𝑜) ×
(2nd ‘𝑜)))) |
| 8 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = (2nd ‘𝑜) → ((Base‘𝑟) ↑m 𝑛) = ((Base‘𝑟) ↑m
(2nd ‘𝑜))) |
| 9 | 8 | adantl 481 |
. . . . . 6
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → ((Base‘𝑟) ↑m 𝑛) = ((Base‘𝑟) ↑m (2nd
‘𝑜))) |
| 10 | | simpl 482 |
. . . . . . 7
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → 𝑚 = (1st ‘𝑜)) |
| 11 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → 𝑛 = (2nd ‘𝑜)) |
| 12 | 11 | mpteq1d 5237 |
. . . . . . . 8
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))) = (𝑗 ∈ (2nd ‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))) |
| 13 | 12 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))) = (𝑟 Σg (𝑗 ∈ (2nd
‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))) |
| 14 | 10, 13 | mpteq12dv 5233 |
. . . . . 6
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))) = (𝑖 ∈ (1st ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) |
| 15 | 7, 9, 14 | mpoeq123dv 7508 |
. . . . 5
⊢ ((𝑚 = (1st ‘𝑜) ∧ 𝑛 = (2nd ‘𝑜)) → (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) = (𝑥 ∈ ((Base‘𝑟) ↑m ((1st
‘𝑜) ×
(2nd ‘𝑜))), 𝑦 ∈ ((Base‘𝑟) ↑m (2nd
‘𝑜)) ↦ (𝑖 ∈ (1st
‘𝑜) ↦ (𝑟 Σg
(𝑗 ∈ (2nd
‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))) |
| 16 | 4, 5, 15 | csbie2 3938 |
. . . 4
⊢
⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd
‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) = (𝑥 ∈ ((Base‘𝑟) ↑m ((1st
‘𝑜) ×
(2nd ‘𝑜))), 𝑦 ∈ ((Base‘𝑟) ↑m (2nd
‘𝑜)) ↦ (𝑖 ∈ (1st
‘𝑜) ↦ (𝑟 Σg
(𝑗 ∈ (2nd
‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) |
| 17 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → 𝑟 = 𝑅) |
| 18 | 17 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (Base‘𝑟) = (Base‘𝑅)) |
| 19 | | mvmulfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
| 20 | 18, 19 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (Base‘𝑟) = 𝐵) |
| 21 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑜 = 〈𝑀, 𝑁〉 → (1st ‘𝑜) = (1st
‘〈𝑀, 𝑁〉)) |
| 22 | 21 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (1st ‘𝑜) = (1st
‘〈𝑀, 𝑁〉)) |
| 23 | | mvmulfval.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ Fin) |
| 24 | | mvmulfval.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 25 | | op1stg 8026 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) →
(1st ‘〈𝑀, 𝑁〉) = 𝑀) |
| 26 | 23, 24, 25 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘〈𝑀, 𝑁〉) = 𝑀) |
| 27 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (1st
‘〈𝑀, 𝑁〉) = 𝑀) |
| 28 | 22, 27 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (1st ‘𝑜) = 𝑀) |
| 29 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑜 = 〈𝑀, 𝑁〉 → (2nd ‘𝑜) = (2nd
‘〈𝑀, 𝑁〉)) |
| 30 | 29 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (2nd ‘𝑜) = (2nd
‘〈𝑀, 𝑁〉)) |
| 31 | | op2ndg 8027 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) →
(2nd ‘〈𝑀, 𝑁〉) = 𝑁) |
| 32 | 23, 24, 31 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝑀, 𝑁〉) = 𝑁) |
| 33 | 32 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (2nd
‘〈𝑀, 𝑁〉) = 𝑁) |
| 34 | 30, 33 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (2nd ‘𝑜) = 𝑁) |
| 35 | 28, 34 | xpeq12d 5716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → ((1st
‘𝑜) ×
(2nd ‘𝑜))
= (𝑀 × 𝑁)) |
| 36 | 20, 35 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → ((Base‘𝑟) ↑m
((1st ‘𝑜)
× (2nd ‘𝑜))) = (𝐵 ↑m (𝑀 × 𝑁))) |
| 37 | 20, 34 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → ((Base‘𝑟) ↑m
(2nd ‘𝑜))
= (𝐵 ↑m
𝑁)) |
| 38 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉) → (.r‘𝑟) = (.r‘𝑅)) |
| 40 | 39 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (.r‘𝑟) = (.r‘𝑅)) |
| 41 | | mvmulfval.t |
. . . . . . . . . 10
⊢ · =
(.r‘𝑅) |
| 42 | 40, 41 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (.r‘𝑟) = · ) |
| 43 | 42 | oveqd 7448 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)) = ((𝑖𝑥𝑗) · (𝑦‘𝑗))) |
| 44 | 34, 43 | mpteq12dv 5233 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (𝑗 ∈ (2nd ‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗)))) |
| 45 | 17, 44 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (𝑟 Σg (𝑗 ∈ (2nd
‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))) |
| 46 | 28, 45 | mpteq12dv 5233 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (𝑖 ∈ (1st ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))) = (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗)))))) |
| 47 | 36, 37, 46 | mpoeq123dv 7508 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) → (𝑥 ∈ ((Base‘𝑟) ↑m ((1st
‘𝑜) ×
(2nd ‘𝑜))), 𝑦 ∈ ((Base‘𝑟) ↑m (2nd
‘𝑜)) ↦ (𝑖 ∈ (1st
‘𝑜) ↦ (𝑟 Σg
(𝑗 ∈ (2nd
‘𝑜) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))))) |
| 48 | 16, 47 | eqtrid 2789 |
. . 3
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁〉)) →
⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd
‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))))) |
| 49 | | mvmulfval.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
| 50 | 49 | elexd 3504 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
| 51 | | opex 5469 |
. . . 4
⊢
〈𝑀, 𝑁〉 ∈ V |
| 52 | 51 | a1i 11 |
. . 3
⊢ (𝜑 → 〈𝑀, 𝑁〉 ∈ V) |
| 53 | | ovex 7464 |
. . . . 5
⊢ (𝐵 ↑m (𝑀 × 𝑁)) ∈ V |
| 54 | | ovex 7464 |
. . . . 5
⊢ (𝐵 ↑m 𝑁) ∈ V |
| 55 | 53, 54 | mpoex 8104 |
. . . 4
⊢ (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗)))))) ∈ V |
| 56 | 55 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗)))))) ∈ V) |
| 57 | 3, 48, 50, 52, 56 | ovmpod 7585 |
. 2
⊢ (𝜑 → (𝑅 maVecMul 〈𝑀, 𝑁〉) = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))))) |
| 58 | 1, 57 | eqtrid 2789 |
1
⊢ (𝜑 → × = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))))) |