Step | Hyp | Ref
| Expression |
1 | | 1mavmul.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | 1mavmul.t |
. . 3
⊢ · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) |
3 | | 1mavmul.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
4 | | eqid 2610 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
5 | | 1mavmul.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | | 1mavmul.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ Fin) |
7 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝐴) =
(Base‘𝐴) |
8 | 1 | fveq2i 6106 |
. . . . 5
⊢
(1r‘𝐴) = (1r‘(𝑁 Mat 𝑅)) |
9 | 1, 7, 8 | mat1bas 20074 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) →
(1r‘𝐴)
∈ (Base‘𝐴)) |
10 | 5, 6, 9 | syl2anc 691 |
. . 3
⊢ (𝜑 → (1r‘𝐴) ∈ (Base‘𝐴)) |
11 | | 1mavmul.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) |
12 | 1, 2, 3, 4, 5, 6, 10, 11 | mavmulval 20170 |
. 2
⊢ (𝜑 →
((1r‘𝐴)
·
𝑌) = (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)))))) |
13 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) |
14 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
15 | 1, 13, 14 | mat1 20072 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))) |
16 | 6, 5, 15 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝐴) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))) |
17 | 16 | oveqdr 6573 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑖(1r‘𝐴)𝑗) = (𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)) |
18 | 17 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)) = ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗))) |
19 | 18 | mpteq2dv 4673 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗))) = (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)))) |
20 | 19 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗))))) |
21 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅))) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))) |
22 | | eqeq12 2623 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥 = 𝑦 ↔ 𝑖 = 𝑗)) |
23 | 22 | ifbid 4058 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) |
24 | 23 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ (𝑥 = 𝑖 ∧ 𝑦 = 𝑗)) → if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) |
25 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
27 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
28 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) ∈ V |
29 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (1r‘𝑅) ∈ V) |
30 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
32 | 29, 31 | ifcld 4081 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) ∈ V) |
33 | 21, 24, 26, 27, 32 | ovmpt2d 6686 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) |
34 | 33 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)) = (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗))) |
35 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅)) |
36 | 35 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅)) |
37 | 36 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗))) |
38 | 5 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑅 ∈ Ring) |
39 | 38 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
40 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑅)
∈ V |
41 | 3, 40 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 ∈ V |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ V) |
43 | 42, 6 | elmapd 7758 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑𝑚 𝑁) ↔ 𝑌:𝑁⟶𝐵)) |
44 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑌:𝑁⟶𝐵 ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) |
45 | 44 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌:𝑁⟶𝐵 → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) |
46 | 43, 45 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑𝑚 𝑁) → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵))) |
47 | 11, 46 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) |
49 | 48 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) |
50 | 3, 4, 13 | ringlidm 18394 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑗) ∈ 𝐵) → ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑗)) |
51 | 39, 49, 50 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑗)) |
52 | 51 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → ((1r‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑗)) |
53 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → (𝑌‘𝑗) = (𝑌‘𝑖)) |
54 | 53 | equcoms 1934 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝑌‘𝑗) = (𝑌‘𝑖)) |
55 | 54 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (𝑌‘𝑗) = (𝑌‘𝑖)) |
56 | 37, 52, 55 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = (𝑌‘𝑖)) |
57 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (𝑌‘𝑖)) |
58 | 57 | equcoms 1934 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (𝑌‘𝑖)) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (𝑌‘𝑖)) |
60 | 56, 59 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) |
61 | | iffalse 4045 |
. . . . . . . . . . 11
⊢ (¬
𝑖 = 𝑗 → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
62 | 61 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (¬
𝑖 = 𝑗 → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗))) |
63 | 62 | adantr 480 |
. . . . . . . . 9
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗))) |
64 | 3, 4, 14 | ringlz 18410 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑗) ∈ 𝐵) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (0g‘𝑅)) |
65 | 39, 49, 64 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (0g‘𝑅)) |
66 | 65 | adantl 481 |
. . . . . . . . 9
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑗)) = (0g‘𝑅)) |
67 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 ↔ 𝑗 = 𝑖) |
68 | | iffalse 4045 |
. . . . . . . . . . . 12
⊢ (¬
𝑗 = 𝑖 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (0g‘𝑅)) |
69 | 67, 68 | sylnbi 319 |
. . . . . . . . . . 11
⊢ (¬
𝑖 = 𝑗 → if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)) = (0g‘𝑅)) |
70 | 69 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (¬
𝑖 = 𝑗 → (0g‘𝑅) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) |
71 | 70 | adantr 480 |
. . . . . . . . 9
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (0g‘𝑅) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) |
72 | 63, 66, 71 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((¬
𝑖 = 𝑗 ∧ ((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁)) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) |
73 | 60, 72 | pm2.61ian 827 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) |
74 | 34, 73 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)) = if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) |
75 | 74 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗))) = (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)))) |
76 | 75 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, (1r‘𝑅), (0g‘𝑅)))𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))))) |
77 | | ringmnd 18379 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
78 | 5, 77 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Mnd) |
79 | 78 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑅 ∈ Mnd) |
80 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑁 ∈ Fin) |
81 | | eqid 2610 |
. . . . 5
⊢ (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) = (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅))) |
82 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝑌:𝑁⟶𝐵 ∧ 𝑖 ∈ 𝑁) → (𝑌‘𝑖) ∈ 𝐵) |
83 | 82, 3 | syl6eleq 2698 |
. . . . . . . . 9
⊢ ((𝑌:𝑁⟶𝐵 ∧ 𝑖 ∈ 𝑁) → (𝑌‘𝑖) ∈ (Base‘𝑅)) |
84 | 83 | ex 449 |
. . . . . . . 8
⊢ (𝑌:𝑁⟶𝐵 → (𝑖 ∈ 𝑁 → (𝑌‘𝑖) ∈ (Base‘𝑅))) |
85 | 43, 84 | syl6bi 242 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑𝑚 𝑁) → (𝑖 ∈ 𝑁 → (𝑌‘𝑖) ∈ (Base‘𝑅)))) |
86 | 11, 85 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ 𝑁 → (𝑌‘𝑖) ∈ (Base‘𝑅))) |
87 | 86 | imp 444 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑌‘𝑖) ∈ (Base‘𝑅)) |
88 | 14, 79, 80, 25, 81, 87 | gsummptif1n0 18188 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑖, (𝑌‘𝑖), (0g‘𝑅)))) = (𝑌‘𝑖)) |
89 | 20, 76, 88 | 3eqtrd 2648 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑌‘𝑖)) |
90 | 89 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(1r‘𝐴)𝑗)(.r‘𝑅)(𝑌‘𝑗))))) = (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖))) |
91 | | ffn 5958 |
. . . . 5
⊢ (𝑌:𝑁⟶𝐵 → 𝑌 Fn 𝑁) |
92 | 43, 91 | syl6bi 242 |
. . . 4
⊢ (𝜑 → (𝑌 ∈ (𝐵 ↑𝑚 𝑁) → 𝑌 Fn 𝑁)) |
93 | 11, 92 | mpd 15 |
. . 3
⊢ (𝜑 → 𝑌 Fn 𝑁) |
94 | | eqcom 2617 |
. . . 4
⊢ ((𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖)) = 𝑌 ↔ 𝑌 = (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖))) |
95 | | dffn5 6151 |
. . . 4
⊢ (𝑌 Fn 𝑁 ↔ 𝑌 = (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖))) |
96 | 94, 95 | bitr4i 266 |
. . 3
⊢ ((𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖)) = 𝑌 ↔ 𝑌 Fn 𝑁) |
97 | 93, 96 | sylibr 223 |
. 2
⊢ (𝜑 → (𝑖 ∈ 𝑁 ↦ (𝑌‘𝑖)) = 𝑌) |
98 | 12, 90, 97 | 3eqtrd 2648 |
1
⊢ (𝜑 →
((1r‘𝐴)
·
𝑌) = 𝑌) |