Step | Hyp | Ref
| Expression |
1 | | 1mavmul.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | 1mavmul.t |
. . . 4
⊢ · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) |
3 | | 1mavmul.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
4 | | eqid 2610 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
5 | | 1mavmul.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | | 1mavmul.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Fin) |
7 | | mavmulass.m |
. . . . . 6
⊢ × =
(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
8 | | mavmulass.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) |
9 | 1, 3 | matbas2 20046 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐵 ↑𝑚
(𝑁 × 𝑁)) = (Base‘𝐴)) |
10 | 6, 5, 9 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ↑𝑚 (𝑁 × 𝑁)) = (Base‘𝐴)) |
11 | 8, 10 | eleqtrrd 2691 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑁))) |
12 | | mavmulass.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴)) |
13 | 12, 10 | eleqtrrd 2691 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑁))) |
14 | 3, 5, 7, 6, 6, 6, 11, 13 | mamucl 20026 |
. . . . 5
⊢ (𝜑 → (𝑋 × 𝑍) ∈ (𝐵 ↑𝑚 (𝑁 × 𝑁))) |
15 | 14, 10 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → (𝑋 × 𝑍) ∈ (Base‘𝐴)) |
16 | | 1mavmul.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) |
17 | 1, 2, 3, 4, 5, 6, 15, 16 | mavmulcl 20172 |
. . 3
⊢ (𝜑 → ((𝑋 × 𝑍) · 𝑌) ∈ (𝐵 ↑𝑚 𝑁)) |
18 | | elmapi 7765 |
. . 3
⊢ (((𝑋 × 𝑍) · 𝑌) ∈ (𝐵 ↑𝑚 𝑁) → ((𝑋 × 𝑍) · 𝑌):𝑁⟶𝐵) |
19 | | ffn 5958 |
. . 3
⊢ (((𝑋 × 𝑍) · 𝑌):𝑁⟶𝐵 → ((𝑋 × 𝑍) · 𝑌) Fn 𝑁) |
20 | 17, 18, 19 | 3syl 18 |
. 2
⊢ (𝜑 → ((𝑋 × 𝑍) · 𝑌) Fn 𝑁) |
21 | 1, 2, 3, 4, 5, 6, 12, 16 | mavmulcl 20172 |
. . . 4
⊢ (𝜑 → (𝑍 · 𝑌) ∈ (𝐵 ↑𝑚 𝑁)) |
22 | 1, 2, 3, 4, 5, 6, 8, 21 | mavmulcl 20172 |
. . 3
⊢ (𝜑 → (𝑋 · (𝑍 · 𝑌)) ∈ (𝐵 ↑𝑚 𝑁)) |
23 | | elmapi 7765 |
. . 3
⊢ ((𝑋 · (𝑍 · 𝑌)) ∈ (𝐵 ↑𝑚 𝑁) → (𝑋 · (𝑍 · 𝑌)):𝑁⟶𝐵) |
24 | | ffn 5958 |
. . 3
⊢ ((𝑋 · (𝑍 · 𝑌)):𝑁⟶𝐵 → (𝑋 · (𝑍 · 𝑌)) Fn 𝑁) |
25 | 22, 23, 24 | 3syl 18 |
. 2
⊢ (𝜑 → (𝑋 · (𝑍 · 𝑌)) Fn 𝑁) |
26 | | ringcmn 18404 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
27 | 5, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
28 | 27 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑅 ∈ CMnd) |
29 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑁 ∈ Fin) |
30 | 5 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → 𝑅 ∈ Ring) |
31 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝑋 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶𝐵) |
32 | 11, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋:(𝑁 × 𝑁)⟶𝐵) |
33 | 32 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → 𝑋:(𝑁 × 𝑁)⟶𝐵) |
34 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → 𝑖 ∈ 𝑁) |
35 | | simprr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → 𝑘 ∈ 𝑁) |
36 | 33, 34, 35 | fovrnd 6704 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → (𝑖𝑋𝑘) ∈ 𝐵) |
37 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶𝐵) |
38 | 13, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍:(𝑁 × 𝑁)⟶𝐵) |
39 | 38 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → 𝑍:(𝑁 × 𝑁)⟶𝐵) |
40 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → 𝑗 ∈ 𝑁) |
41 | 39, 35, 40 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → (𝑘𝑍𝑗) ∈ 𝐵) |
42 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝐵 ↑𝑚 𝑁) → 𝑌:𝑁⟶𝐵) |
43 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝑌:𝑁⟶𝐵 ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) |
44 | 43 | ex 449 |
. . . . . . . . . 10
⊢ (𝑌:𝑁⟶𝐵 → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) |
45 | 16, 42, 44 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) |
46 | 45 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) |
47 | 46 | ad2ant2r 779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → (𝑌‘𝑗) ∈ 𝐵) |
48 | 3, 4 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑘𝑍𝑗) ∈ 𝐵 ∧ (𝑌‘𝑗) ∈ 𝐵) → ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)) ∈ 𝐵) |
49 | 30, 41, 47, 48 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)) ∈ 𝐵) |
50 | 3, 4 | ringcl 18384 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑋𝑘) ∈ 𝐵 ∧ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)) ∈ 𝐵) → ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))) ∈ 𝐵) |
51 | 30, 36, 49, 50 | syl3anc 1318 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))) ∈ 𝐵) |
52 | 3, 28, 29, 29, 51 | gsumcom3fi 20025 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))))))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))))) |
53 | 5 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
54 | 6 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑁 ∈ Fin) |
55 | 11 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑁))) |
56 | 13 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑁))) |
57 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
58 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
59 | 7, 3, 4, 53, 54, 54, 54, 55, 56, 57, 58 | mamufv 20012 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑋 × 𝑍)𝑗) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))))) |
60 | 59 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑋 × 𝑍)𝑗)(.r‘𝑅)(𝑌‘𝑗)) = ((𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))))(.r‘𝑅)(𝑌‘𝑗))) |
61 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
62 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑅) |
63 | 46 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) |
64 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑅 ∈ Ring) |
65 | 64 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑅 ∈ Ring) |
66 | 32 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑋:(𝑁 × 𝑁)⟶𝐵) |
67 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
68 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
69 | 66, 67, 68 | fovrnd 6704 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (𝑖𝑋𝑘) ∈ 𝐵) |
70 | 69 | adantlr 747 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (𝑖𝑋𝑘) ∈ 𝐵) |
71 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐵) |
72 | 71 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐵) |
73 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
74 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
75 | 72, 73, 74 | fovrnd 6704 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (𝑘𝑍𝑗) ∈ 𝐵) |
76 | 3, 4 | ringcl 18384 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑋𝑘) ∈ 𝐵 ∧ (𝑘𝑍𝑗) ∈ 𝐵) → ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗)) ∈ 𝐵) |
77 | 65, 70, 75, 76 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗)) ∈ 𝐵) |
78 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))) = (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))) |
79 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗)) ∈ V |
80 | 79 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗)) ∈ V) |
81 | | fvex 6113 |
. . . . . . . . . 10
⊢
(0g‘𝑅) ∈ V |
82 | 81 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
83 | 78, 54, 80, 82 | fsuppmptdm 8169 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))) finSupp (0g‘𝑅)) |
84 | 3, 61, 62, 4, 53, 54, 63, 77, 83 | gsummulc1 18429 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))(.r‘𝑅)(𝑌‘𝑗)))) = ((𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))))(.r‘𝑅)(𝑌‘𝑗))) |
85 | 3, 4 | ringass 18387 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ ((𝑖𝑋𝑘) ∈ 𝐵 ∧ (𝑘𝑍𝑗) ∈ 𝐵 ∧ (𝑌‘𝑗) ∈ 𝐵)) → (((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))(.r‘𝑅)(𝑌‘𝑗)) = ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))) |
86 | 30, 36, 41, 47, 85 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ (𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁)) → (((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))(.r‘𝑅)(𝑌‘𝑗)) = ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))) |
87 | 86 | anassrs 678 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))(.r‘𝑅)(𝑌‘𝑗)) = ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))) |
88 | 87 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ 𝑁 ↦ (((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))(.r‘𝑅)(𝑌‘𝑗))) = (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))))) |
89 | 88 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (((𝑖𝑋𝑘)(.r‘𝑅)(𝑘𝑍𝑗))(.r‘𝑅)(𝑌‘𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))) |
90 | 60, 84, 89 | 3eqtr2d 2650 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑋 × 𝑍)𝑗)(.r‘𝑅)(𝑌‘𝑗)) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))) |
91 | 90 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 × 𝑍)𝑗)(.r‘𝑅)(𝑌‘𝑗))) = (𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))))))) |
92 | 91 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 × 𝑍)𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))))) |
93 | 5 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑅 ∈ Ring) |
94 | 6 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑁 ∈ Fin) |
95 | 12 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑍 ∈ (Base‘𝐴)) |
96 | 16 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) |
97 | 1, 2, 3, 4, 93, 94, 95, 96, 68 | mavmulfv 20171 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → ((𝑍 · 𝑌)‘𝑘) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))))) |
98 | 97 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → ((𝑖𝑋𝑘)(.r‘𝑅)((𝑍 · 𝑌)‘𝑘)) = ((𝑖𝑋𝑘)(.r‘𝑅)(𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))) |
99 | 64 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
100 | 71 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑍:(𝑁 × 𝑁)⟶𝐵) |
101 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
102 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
103 | 100, 101,
102 | fovrnd 6704 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑘𝑍𝑗) ∈ 𝐵) |
104 | 45 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (𝑗 ∈ 𝑁 → (𝑌‘𝑗) ∈ 𝐵)) |
105 | 104 | imp 444 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → (𝑌‘𝑗) ∈ 𝐵) |
106 | 99, 103, 105, 48 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)) ∈ 𝐵) |
107 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑁 ↦ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))) = (𝑗 ∈ 𝑁 ↦ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))) |
108 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)) ∈ V |
109 | 108 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)) ∈ V) |
110 | 81 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
111 | 107, 94, 109, 110 | fsuppmptdm 8169 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (𝑗 ∈ 𝑁 ↦ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))) finSupp (0g‘𝑅)) |
112 | 3, 61, 62, 4, 93, 94, 69, 106, 111 | gsummulc2 18430 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))))) = ((𝑖𝑋𝑘)(.r‘𝑅)(𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))) |
113 | 98, 112 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → ((𝑖𝑋𝑘)(.r‘𝑅)((𝑍 · 𝑌)‘𝑘)) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))) |
114 | 113 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑍 · 𝑌)‘𝑘))) = (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗))))))) |
115 | 114 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑍 · 𝑌)‘𝑘)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑘𝑍𝑗)(.r‘𝑅)(𝑌‘𝑗)))))))) |
116 | 52, 92, 115 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 × 𝑍)𝑗)(.r‘𝑅)(𝑌‘𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑍 · 𝑌)‘𝑘))))) |
117 | 15 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑋 × 𝑍) ∈ (Base‘𝐴)) |
118 | 16 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) |
119 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
120 | 1, 2, 3, 4, 64, 29, 117, 118, 119 | mavmulfv 20171 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (((𝑋 × 𝑍) · 𝑌)‘𝑖) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖(𝑋 × 𝑍)𝑗)(.r‘𝑅)(𝑌‘𝑗))))) |
121 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ (Base‘𝐴)) |
122 | 21 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (𝑍 · 𝑌) ∈ (𝐵 ↑𝑚 𝑁)) |
123 | 1, 2, 3, 4, 64, 29, 121, 122, 119 | mavmulfv 20171 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → ((𝑋 · (𝑍 · 𝑌))‘𝑖) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑋𝑘)(.r‘𝑅)((𝑍 · 𝑌)‘𝑘))))) |
124 | 116, 120,
123 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → (((𝑋 × 𝑍) · 𝑌)‘𝑖) = ((𝑋 · (𝑍 · 𝑌))‘𝑖)) |
125 | 20, 25, 124 | eqfnfvd 6222 |
1
⊢ (𝜑 → ((𝑋 × 𝑍) · 𝑌) = (𝑋 · (𝑍 · 𝑌))) |