| Step | Hyp | Ref
| Expression |
| 1 | | mamufval.f |
. 2
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) |
| 2 | | df-mamu 22395 |
. . . 4
⊢ maMul =
(𝑟 ∈ V, 𝑜 ∈ V ↦
⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd
‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd
‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))) |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → maMul = (𝑟 ∈ V, 𝑜 ∈ V ↦
⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd
‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd
‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))))) |
| 4 | | fvex 6919 |
. . . . 5
⊢
(1st ‘(1st ‘𝑜)) ∈ V |
| 5 | | fvex 6919 |
. . . . 5
⊢
(2nd ‘(1st ‘𝑜)) ∈ V |
| 6 | | fvex 6919 |
. . . . . . 7
⊢
(2nd ‘𝑜) ∈ V |
| 7 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑝 = (2nd ‘𝑜) → ((Base‘𝑟) ↑m (𝑚 × 𝑛)) = ((Base‘𝑟) ↑m (𝑚 × 𝑛))) |
| 8 | | xpeq2 5706 |
. . . . . . . . 9
⊢ (𝑝 = (2nd ‘𝑜) → (𝑛 × 𝑝) = (𝑛 × (2nd ‘𝑜))) |
| 9 | 8 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑝 = (2nd ‘𝑜) → ((Base‘𝑟) ↑m (𝑛 × 𝑝)) = ((Base‘𝑟) ↑m (𝑛 × (2nd ‘𝑜)))) |
| 10 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑝 = (2nd ‘𝑜) → 𝑚 = 𝑚) |
| 11 | | id 22 |
. . . . . . . . 9
⊢ (𝑝 = (2nd ‘𝑜) → 𝑝 = (2nd ‘𝑜)) |
| 12 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑝 = (2nd ‘𝑜) → (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))) |
| 13 | 10, 11, 12 | mpoeq123dv 7508 |
. . . . . . . 8
⊢ (𝑝 = (2nd ‘𝑜) → (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑚, 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) |
| 14 | 7, 9, 13 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (𝑝 = (2nd ‘𝑜) → (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × (2nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))) |
| 15 | 6, 14 | csbie 3934 |
. . . . . 6
⊢
⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × (2nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) |
| 16 | | xpeq12 5710 |
. . . . . . . 8
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → (𝑚 × 𝑛) = ((1st ‘(1st
‘𝑜)) ×
(2nd ‘(1st ‘𝑜)))) |
| 17 | 16 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) →
((Base‘𝑟)
↑m (𝑚
× 𝑛)) =
((Base‘𝑟)
↑m ((1st ‘(1st ‘𝑜)) × (2nd
‘(1st ‘𝑜))))) |
| 18 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → 𝑛 = (2nd
‘(1st ‘𝑜))) |
| 19 | 18 | xpeq1d 5714 |
. . . . . . . 8
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → (𝑛 × (2nd
‘𝑜)) =
((2nd ‘(1st ‘𝑜)) × (2nd ‘𝑜))) |
| 20 | 19 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) →
((Base‘𝑟)
↑m (𝑛
× (2nd ‘𝑜))) = ((Base‘𝑟) ↑m ((2nd
‘(1st ‘𝑜)) × (2nd ‘𝑜)))) |
| 21 | | id 22 |
. . . . . . . . 9
⊢ (𝑚 = (1st
‘(1st ‘𝑜)) → 𝑚 = (1st ‘(1st
‘𝑜))) |
| 22 | 21 | adantr 480 |
. . . . . . . 8
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → 𝑚 = (1st
‘(1st ‘𝑜))) |
| 23 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) →
(2nd ‘𝑜) =
(2nd ‘𝑜)) |
| 24 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))) |
| 25 | 18, 24 | mpteq12dv 5233 |
. . . . . . . . 9
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))) |
| 26 | 25 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → (𝑟 Σg
(𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))) = (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))) |
| 27 | 22, 23, 26 | mpoeq123dv 7508 |
. . . . . . 7
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → (𝑖 ∈ 𝑚, 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ (1st
‘(1st ‘𝑜)), 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) |
| 28 | 17, 20, 27 | mpoeq123dv 7508 |
. . . . . 6
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) → (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × (2nd ‘𝑜))) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑m ((1st
‘(1st ‘𝑜)) × (2nd
‘(1st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑m ((2nd
‘(1st ‘𝑜)) × (2nd ‘𝑜))) ↦ (𝑖 ∈ (1st
‘(1st ‘𝑜)), 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))) |
| 29 | 15, 28 | eqtrid 2789 |
. . . . 5
⊢ ((𝑚 = (1st
‘(1st ‘𝑜)) ∧ 𝑛 = (2nd ‘(1st
‘𝑜))) →
⦋(2nd ‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑m ((1st
‘(1st ‘𝑜)) × (2nd
‘(1st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑m ((2nd
‘(1st ‘𝑜)) × (2nd ‘𝑜))) ↦ (𝑖 ∈ (1st
‘(1st ‘𝑜)), 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))))) |
| 30 | 4, 5, 29 | csbie2 3938 |
. . . 4
⊢
⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd
‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd
‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ ((Base‘𝑟) ↑m ((1st
‘(1st ‘𝑜)) × (2nd
‘(1st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑m ((2nd
‘(1st ‘𝑜)) × (2nd ‘𝑜))) ↦ (𝑖 ∈ (1st
‘(1st ‘𝑜)), 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) |
| 31 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → 𝑟 = 𝑅) |
| 32 | 31 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (Base‘𝑟) = (Base‘𝑅)) |
| 33 | | mamufval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
| 34 | 32, 33 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (Base‘𝑟) = 𝐵) |
| 35 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑜 = 〈𝑀, 𝑁, 𝑃〉 → (1st ‘𝑜) = (1st
‘〈𝑀, 𝑁, 𝑃〉)) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑜 = 〈𝑀, 𝑁, 𝑃〉 → (1st
‘(1st ‘𝑜)) = (1st ‘(1st
‘〈𝑀, 𝑁, 𝑃〉))) |
| 37 | 36 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (1st
‘(1st ‘𝑜)) = (1st ‘(1st
‘〈𝑀, 𝑁, 𝑃〉))) |
| 38 | | mamufval.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ Fin) |
| 39 | | mamufval.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 40 | | mamufval.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ Fin) |
| 41 | | ot1stg 8028 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) →
(1st ‘(1st ‘〈𝑀, 𝑁, 𝑃〉)) = 𝑀) |
| 42 | 38, 39, 40, 41 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘(1st ‘〈𝑀, 𝑁, 𝑃〉)) = 𝑀) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (1st
‘(1st ‘〈𝑀, 𝑁, 𝑃〉)) = 𝑀) |
| 44 | 37, 43 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (1st
‘(1st ‘𝑜)) = 𝑀) |
| 45 | 35 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑜 = 〈𝑀, 𝑁, 𝑃〉 → (2nd
‘(1st ‘𝑜)) = (2nd ‘(1st
‘〈𝑀, 𝑁, 𝑃〉))) |
| 46 | 45 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (2nd
‘(1st ‘𝑜)) = (2nd ‘(1st
‘〈𝑀, 𝑁, 𝑃〉))) |
| 47 | | ot2ndg 8029 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin) →
(2nd ‘(1st ‘〈𝑀, 𝑁, 𝑃〉)) = 𝑁) |
| 48 | 38, 39, 40, 47 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘(1st ‘〈𝑀, 𝑁, 𝑃〉)) = 𝑁) |
| 49 | 48 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (2nd
‘(1st ‘〈𝑀, 𝑁, 𝑃〉)) = 𝑁) |
| 50 | 46, 49 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (2nd
‘(1st ‘𝑜)) = 𝑁) |
| 51 | 44, 50 | xpeq12d 5716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → ((1st
‘(1st ‘𝑜)) × (2nd
‘(1st ‘𝑜))) = (𝑀 × 𝑁)) |
| 52 | 34, 51 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → ((Base‘𝑟) ↑m
((1st ‘(1st ‘𝑜)) × (2nd
‘(1st ‘𝑜)))) = (𝐵 ↑m (𝑀 × 𝑁))) |
| 53 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑜 = 〈𝑀, 𝑁, 𝑃〉 → (2nd ‘𝑜) = (2nd
‘〈𝑀, 𝑁, 𝑃〉)) |
| 54 | 53 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (2nd ‘𝑜) = (2nd
‘〈𝑀, 𝑁, 𝑃〉)) |
| 55 | | ot3rdg 8030 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Fin →
(2nd ‘〈𝑀, 𝑁, 𝑃〉) = 𝑃) |
| 56 | 40, 55 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝑀, 𝑁, 𝑃〉) = 𝑃) |
| 57 | 56 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (2nd
‘〈𝑀, 𝑁, 𝑃〉) = 𝑃) |
| 58 | 54, 57 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (2nd ‘𝑜) = 𝑃) |
| 59 | 50, 58 | xpeq12d 5716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → ((2nd
‘(1st ‘𝑜)) × (2nd ‘𝑜)) = (𝑁 × 𝑃)) |
| 60 | 34, 59 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → ((Base‘𝑟) ↑m
((2nd ‘(1st ‘𝑜)) × (2nd ‘𝑜))) = (𝐵 ↑m (𝑁 × 𝑃))) |
| 61 | 31 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (.r‘𝑟) = (.r‘𝑅)) |
| 62 | | mamufval.t |
. . . . . . . . . 10
⊢ · =
(.r‘𝑅) |
| 63 | 61, 62 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (.r‘𝑟) = · ) |
| 64 | 63 | oveqd 7448 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)) = ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))) |
| 65 | 50, 64 | mpteq12dv 5233 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))) = (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))) |
| 66 | 31, 65 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))) |
| 67 | 44, 58, 66 | mpoeq123dv 7508 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (𝑖 ∈ (1st
‘(1st ‘𝑜)), 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘))))) = (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) |
| 68 | 52, 60, 67 | mpoeq123dv 7508 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) → (𝑥 ∈ ((Base‘𝑟) ↑m ((1st
‘(1st ‘𝑜)) × (2nd
‘(1st ‘𝑜)))), 𝑦 ∈ ((Base‘𝑟) ↑m ((2nd
‘(1st ‘𝑜)) × (2nd ‘𝑜))) ↦ (𝑖 ∈ (1st
‘(1st ‘𝑜)), 𝑘 ∈ (2nd ‘𝑜) ↦ (𝑟 Σg (𝑗 ∈ (2nd
‘(1st ‘𝑜)) ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))) |
| 69 | 30, 68 | eqtrid 2789 |
. . 3
⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑜 = 〈𝑀, 𝑁, 𝑃〉)) →
⦋(1st ‘(1st ‘𝑜)) / 𝑚⦌⦋(2nd
‘(1st ‘𝑜)) / 𝑛⦌⦋(2nd
‘𝑜) / 𝑝⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m (𝑛 × 𝑝)) ↦ (𝑖 ∈ 𝑚, 𝑘 ∈ 𝑝 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑗𝑦𝑘)))))) = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))) |
| 70 | | mamufval.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
| 71 | 70 | elexd 3504 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
| 72 | | otex 5470 |
. . . 4
⊢
〈𝑀, 𝑁, 𝑃〉 ∈ V |
| 73 | 72 | a1i 11 |
. . 3
⊢ (𝜑 → 〈𝑀, 𝑁, 𝑃〉 ∈ V) |
| 74 | | ovex 7464 |
. . . . 5
⊢ (𝐵 ↑m (𝑀 × 𝑁)) ∈ V |
| 75 | | ovex 7464 |
. . . . 5
⊢ (𝐵 ↑m (𝑁 × 𝑃)) ∈ V |
| 76 | 74, 75 | mpoex 8104 |
. . . 4
⊢ (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V |
| 77 | 76 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘)))))) ∈ V) |
| 78 | 3, 69, 71, 73, 77 | ovmpod 7585 |
. 2
⊢ (𝜑 → (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))) |
| 79 | 1, 78 | eqtrid 2789 |
1
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m (𝑁 × 𝑃)) ↦ (𝑖 ∈ 𝑀, 𝑘 ∈ 𝑃 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑗𝑦𝑘))))))) |