| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mvmumamul1.t | . . . . . 6
⊢  · =
(𝑅 maVecMul 〈𝑀, 𝑁〉) | 
| 2 |  | mvmumamul1.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑅) | 
| 3 |  | eqid 2736 | . . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 4 |  | mvmumamul1.r | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 5 | 4 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → 𝑅 ∈ Ring) | 
| 6 |  | mvmumamul1.m | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ Fin) | 
| 7 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → 𝑀 ∈ Fin) | 
| 8 |  | mvmumamul1.n | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → 𝑁 ∈ Fin) | 
| 10 |  | mvmumamul1.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m (𝑀 × 𝑁))) | 
| 11 | 10 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → 𝐴 ∈ (𝐵 ↑m (𝑀 × 𝑁))) | 
| 12 |  | mvmumamul1.y | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) | 
| 13 | 12 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → 𝑌 ∈ (𝐵 ↑m 𝑁)) | 
| 14 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → 𝑖 ∈ 𝑀) | 
| 15 | 1, 2, 3, 5, 7, 9, 11, 13, 14 | mvmulfv 22551 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → ((𝐴 · 𝑌)‘𝑖) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑌‘𝑘))))) | 
| 16 | 15 | adantlr 715 | . . . 4
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) ∧ 𝑖 ∈ 𝑀) → ((𝐴 · 𝑌)‘𝑖) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑌‘𝑘))))) | 
| 17 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝑌‘𝑗) = (𝑌‘𝑘)) | 
| 18 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝑗𝑍∅) = (𝑘𝑍∅)) | 
| 19 | 17, 18 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝑌‘𝑗) = (𝑗𝑍∅) ↔ (𝑌‘𝑘) = (𝑘𝑍∅))) | 
| 20 | 19 | rspccv 3618 | . . . . . . . . . 10
⊢
(∀𝑗 ∈
𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → (𝑘 ∈ 𝑁 → (𝑌‘𝑘) = (𝑘𝑍∅))) | 
| 21 | 20 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) → (𝑘 ∈ 𝑁 → (𝑌‘𝑘) = (𝑘𝑍∅))) | 
| 22 | 21 | imp 406 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) ∧ 𝑘 ∈ 𝑁) → (𝑌‘𝑘) = (𝑘𝑍∅)) | 
| 23 | 22 | oveq2d 7448 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) ∧ 𝑘 ∈ 𝑁) → ((𝑖𝐴𝑘)(.r‘𝑅)(𝑌‘𝑘)) = ((𝑖𝐴𝑘)(.r‘𝑅)(𝑘𝑍∅))) | 
| 24 | 23 | mpteq2dva 5241 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) → (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑌‘𝑘))) = (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑘𝑍∅)))) | 
| 25 | 24 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑌‘𝑘)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑘𝑍∅))))) | 
| 26 | 25 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) ∧ 𝑖 ∈ 𝑀) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑌‘𝑘)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑘𝑍∅))))) | 
| 27 |  | mvmumamul1.x | . . . . . . 7
⊢  × =
(𝑅 maMul 〈𝑀, 𝑁, {∅}〉) | 
| 28 |  | snfi 9084 | . . . . . . . 8
⊢ {∅}
∈ Fin | 
| 29 | 28 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → {∅} ∈
Fin) | 
| 30 |  | mvmumamul1.z | . . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × {∅}))) | 
| 31 | 30 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → 𝑍 ∈ (𝐵 ↑m (𝑁 × {∅}))) | 
| 32 |  | 0ex 5306 | . . . . . . . . 9
⊢ ∅
∈ V | 
| 33 | 32 | snid 4661 | . . . . . . . 8
⊢ ∅
∈ {∅} | 
| 34 | 33 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → ∅ ∈
{∅}) | 
| 35 | 27, 2, 3, 5, 7, 9, 29, 11, 31, 14, 34 | mamufv 22399 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → (𝑖(𝐴 × 𝑍)∅) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑘𝑍∅))))) | 
| 36 | 35 | eqcomd 2742 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑀) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑘𝑍∅)))) = (𝑖(𝐴 × 𝑍)∅)) | 
| 37 | 36 | adantlr 715 | . . . 4
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) ∧ 𝑖 ∈ 𝑀) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝐴𝑘)(.r‘𝑅)(𝑘𝑍∅)))) = (𝑖(𝐴 × 𝑍)∅)) | 
| 38 | 16, 26, 37 | 3eqtrd 2780 | . . 3
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) ∧ 𝑖 ∈ 𝑀) → ((𝐴 · 𝑌)‘𝑖) = (𝑖(𝐴 × 𝑍)∅)) | 
| 39 | 38 | ralrimiva 3145 | . 2
⊢ ((𝜑 ∧ ∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅)) → ∀𝑖 ∈ 𝑀 ((𝐴 · 𝑌)‘𝑖) = (𝑖(𝐴 × 𝑍)∅)) | 
| 40 | 39 | ex 412 | 1
⊢ (𝜑 → (∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → ∀𝑖 ∈ 𝑀 ((𝐴 · 𝑌)‘𝑖) = (𝑖(𝐴 × 𝑍)∅))) |