| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1mavmul.a | . . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 2 |  | 1mavmul.t | . . 3
⊢  · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) | 
| 3 |  | 1mavmul.b | . . 3
⊢ 𝐵 = (Base‘𝑅) | 
| 4 |  | eqid 2737 | . . 3
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 5 |  | 1mavmul.r | . . 3
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 6 |  | 1mavmul.n | . . 3
⊢ (𝜑 → 𝑁 ∈ Fin) | 
| 7 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝐴) =
(Base‘𝐴) | 
| 8 | 1 | fveq2i 6909 | . . . . 5
⊢
(1r‘𝐴) = (1r‘(𝑁 Mat 𝑅)) | 
| 9 | 1, 7, 8 | mat1bas 22455 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
(1r‘𝐴)
∈ (Base‘𝐴)) | 
| 10 | 5, 6, 9 | syl2anc 584 | . . 3
⊢ (𝜑 → (1r‘𝐴) ∈ (Base‘𝐴)) | 
| 11 |  | 1mavmul.y | . . 3
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) | 
| 12 | 1, 2, 3, 4, 5, 6, 10, 11 | mavmulval 22551 | . 2
⊢ (𝜑 →
((1r‘𝐴)
·
𝑌) = (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)))))) | 
| 13 |  | eqid 2737 | . . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 14 |  | eqid 2737 | . . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 15 | 1, 13, 14 | mat1 22453 | . . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))) | 
| 16 | 6, 5, 15 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (1r‘𝐴) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))) | 
| 17 | 16 | oveqdr 7459 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑖(1r‘𝐴)𝑗) = (𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)) | 
| 18 | 17 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)) = ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗))) | 
| 19 | 18 | mpteq2dv 5244 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗))) = (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)))) | 
| 20 | 19 | oveq2d 7447 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗))))) | 
| 21 |  | eqidd 2738 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅))) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))) | 
| 22 |  | eqeq12 2754 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 = 𝑦 ↔ 𝑖 = 𝑗)) | 
| 23 | 22 | ifbid 4549 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) | 
| 24 | 23 | adantl 481 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ (𝑥 = 𝑖 ∧ 𝑦 = 𝑗)) → if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) | 
| 25 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑖 ∈ 𝑁) | 
| 26 | 25 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) | 
| 27 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) | 
| 28 |  | fvexd 6921 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (1r‘𝑅) ∈ V) | 
| 29 |  | fvexd 6921 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (0g‘𝑅) ∈ V) | 
| 30 | 28, 29 | ifcld 4572 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) ∈ V) | 
| 31 | 21, 24, 26, 27, 30 | ovmpod 7585 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) | 
| 32 | 31 | oveq1d 7446 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)) = (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗))) | 
| 33 |  | iftrue 4531 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅)) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅)) | 
| 35 | 34 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗))) | 
| 36 | 5 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 37 | 36 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 38 | 3 | fvexi 6920 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐵 ∈ V | 
| 39 | 38 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ V) | 
| 40 | 39, 6 | elmapd 8880 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑m 𝑁) ↔ 𝑌:𝑁⟶𝐵)) | 
| 41 |  | ffvelcdm 7101 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑌:𝑁⟶𝐵 ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) | 
| 42 | 41 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝑌:𝑁⟶𝐵 → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) | 
| 43 | 40, 42 | biimtrdi 253 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑m 𝑁) → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵))) | 
| 44 | 11, 43 | mpd 15 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) | 
| 45 | 44 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) | 
| 46 | 45 | imp 406 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) | 
| 47 | 3, 4, 13 | ringlidm 20266 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑗) ∈ 𝐵) → ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑗)) | 
| 48 | 37, 46, 47 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑗)) | 
| 49 | 48 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑗)) | 
| 50 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → (𝑌‘𝑗) = (𝑌‘𝑖)) | 
| 51 | 50 | equcoms 2019 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝑌‘𝑗) = (𝑌‘𝑖)) | 
| 52 | 51 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (𝑌‘𝑗) = (𝑌‘𝑖)) | 
| 53 | 35, 49, 52 | 3eqtrd 2781 | . . . . . . . . 9
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑖)) | 
| 54 |  | iftrue 4531 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (𝑌‘𝑖)) | 
| 55 | 54 | equcoms 2019 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (𝑌‘𝑖)) | 
| 56 | 55 | adantr 480 | . . . . . . . . 9
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (𝑌‘𝑖)) | 
| 57 | 53, 56 | eqtr4d 2780 | . . . . . . . 8
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) | 
| 58 |  | iffalse 4534 | . . . . . . . . . . 11
⊢ (¬
𝑖 = 𝑗 → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) | 
| 59 | 58 | oveq1d 7446 | . . . . . . . . . 10
⊢ (¬
𝑖 = 𝑗 → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗))) | 
| 60 | 59 | adantr 480 | . . . . . . . . 9
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗))) | 
| 61 | 3, 4, 14 | ringlz 20290 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑗) ∈ 𝐵) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (0g‘𝑅)) | 
| 62 | 37, 46, 61 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (0g‘𝑅)) | 
| 63 | 62 | adantl 481 | . . . . . . . . 9
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (0g‘𝑅)) | 
| 64 |  | eqcom 2744 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 ↔ 𝑗 = 𝑖) | 
| 65 |  | iffalse 4534 | . . . . . . . . . . . 12
⊢ (¬
𝑗 = 𝑖 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (0g‘𝑅)) | 
| 66 | 64, 65 | sylnbi 330 | . . . . . . . . . . 11
⊢ (¬
𝑖 = 𝑗 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (0g‘𝑅)) | 
| 67 | 66 | eqcomd 2743 | . . . . . . . . . 10
⊢ (¬
𝑖 = 𝑗 → (0g‘𝑅) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) | 
| 68 | 67 | adantr 480 | . . . . . . . . 9
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (0g‘𝑅) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) | 
| 69 | 60, 63, 68 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) | 
| 70 | 57, 69 | pm2.61ian 812 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) | 
| 71 | 32, 70 | eqtrd 2777 | . . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) | 
| 72 | 71 | mpteq2dva 5242 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗))) = (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)))) | 
| 73 | 72 | oveq2d 7447 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))))) | 
| 74 |  | ringmnd 20240 | . . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 75 | 5, 74 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Mnd) | 
| 76 | 75 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑅 ∈ Mnd) | 
| 77 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑁 ∈ Fin) | 
| 78 |  | eqid 2737 | . . . . 5
⊢ (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) = (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) | 
| 79 |  | ffvelcdm 7101 | . . . . . . . . . 10
⊢ ((𝑌:𝑁⟶𝐵 ∧ 𝑖 ∈ 𝑁) → (𝑌‘𝑖) ∈ 𝐵) | 
| 80 | 79, 3 | eleqtrdi 2851 | . . . . . . . . 9
⊢ ((𝑌:𝑁⟶𝐵 ∧ 𝑖 ∈ 𝑁) → (𝑌‘𝑖) ∈ (Base‘𝑅)) | 
| 81 | 80 | ex 412 | . . . . . . . 8
⊢ (𝑌:𝑁⟶𝐵 → (𝑖 ∈ 𝑁 → (𝑌‘𝑖) ∈ (Base‘𝑅))) | 
| 82 | 40, 81 | biimtrdi 253 | . . . . . . 7
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑m 𝑁) → (𝑖 ∈ 𝑁 → (𝑌‘𝑖) ∈ (Base‘𝑅)))) | 
| 83 | 11, 82 | mpd 15 | . . . . . 6
⊢ (𝜑 → (𝑖 ∈ 𝑁 → (𝑌‘𝑖) ∈ (Base‘𝑅))) | 
| 84 | 83 | imp 406 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑌‘𝑖) ∈ (Base‘𝑅)) | 
| 85 | 14, 76, 77, 25, 78, 84 | gsummptif1n0 19984 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)))) = (𝑌‘𝑖)) | 
| 86 | 20, 73, 85 | 3eqtrd 2781 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑌‘𝑖)) | 
| 87 | 86 | mpteq2dva 5242 | . 2
⊢ (𝜑 → (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗))))) = (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖))) | 
| 88 |  | ffn 6736 | . . . . 5
⊢ (𝑌:𝑁⟶𝐵 → 𝑌 Fn 𝑁) | 
| 89 | 40, 88 | biimtrdi 253 | . . . 4
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑m 𝑁) → 𝑌 Fn 𝑁)) | 
| 90 | 11, 89 | mpd 15 | . . 3
⊢ (𝜑 → 𝑌 Fn 𝑁) | 
| 91 |  | eqcom 2744 | . . . 4
⊢ ((𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖)) = 𝑌 ↔ 𝑌 = (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖))) | 
| 92 |  | dffn5 6967 | . . . 4
⊢ (𝑌 Fn 𝑁 ↔ 𝑌 = (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖))) | 
| 93 | 91, 92 | bitr4i 278 | . . 3
⊢ ((𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖)) = 𝑌 ↔ 𝑌 Fn 𝑁) | 
| 94 | 90, 93 | sylibr 234 | . 2
⊢ (𝜑 → (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖)) = 𝑌) | 
| 95 | 12, 87, 94 | 3eqtrd 2781 | 1
⊢ (𝜑 →
((1r‘𝐴)
·
𝑌) = 𝑌) |