Step | Hyp | Ref
| Expression |
1 | | 1mavmul.a |
. . . 4
Mat |
2 | | 1mavmul.t |
. . . 4
maVecMul |
3 | | 1mavmul.b |
. . . 4
|
4 | | eqid 2622 |
. . . 4
|
5 | | 1mavmul.r |
. . . 4
|
6 | | 1mavmul.n |
. . . 4
|
7 | | mavmulass.m |
. . . . . 6
maMul
|
8 | | mavmulass.x |
. . . . . . 7
|
9 | 1, 3 | matbas2 20227 |
. . . . . . . 8
|
10 | 6, 5, 9 | syl2anc 693 |
. . . . . . 7
|
11 | 8, 10 | eleqtrrd 2704 |
. . . . . 6
|
12 | | mavmulass.z |
. . . . . . 7
|
13 | 12, 10 | eleqtrrd 2704 |
. . . . . 6
|
14 | 3, 5, 7, 6, 6, 6, 11, 13 | mamucl 20207 |
. . . . 5
|
15 | 14, 10 | eleqtrd 2703 |
. . . 4
|
16 | | 1mavmul.y |
. . . 4
|
17 | 1, 2, 3, 4, 5, 6, 15, 16 | mavmulcl 20353 |
. . 3
|
18 | | elmapi 7879 |
. . 3
|
19 | | ffn 6045 |
. . 3
|
20 | 17, 18, 19 | 3syl 18 |
. 2
|
21 | 1, 2, 3, 4, 5, 6, 12, 16 | mavmulcl 20353 |
. . . 4
|
22 | 1, 2, 3, 4, 5, 6, 8, 21 | mavmulcl 20353 |
. . 3
|
23 | | elmapi 7879 |
. . 3
|
24 | | ffn 6045 |
. . 3
|
25 | 22, 23, 24 | 3syl 18 |
. 2
|
26 | | ringcmn 18581 |
. . . . . . 7
CMnd |
27 | 5, 26 | syl 17 |
. . . . . 6
CMnd |
28 | 27 | adantr 481 |
. . . . 5
CMnd |
29 | 6 | adantr 481 |
. . . . 5
|
30 | 5 | ad2antrr 762 |
. . . . . 6
|
31 | | elmapi 7879 |
. . . . . . . . 9
|
32 | 11, 31 | syl 17 |
. . . . . . . 8
|
33 | 32 | ad2antrr 762 |
. . . . . . 7
|
34 | | simplr 792 |
. . . . . . 7
|
35 | | simprr 796 |
. . . . . . 7
|
36 | 33, 34, 35 | fovrnd 6806 |
. . . . . 6
|
37 | | elmapi 7879 |
. . . . . . . . . 10
|
38 | 13, 37 | syl 17 |
. . . . . . . . 9
|
39 | 38 | ad2antrr 762 |
. . . . . . . 8
|
40 | | simprl 794 |
. . . . . . . 8
|
41 | 39, 35, 40 | fovrnd 6806 |
. . . . . . 7
|
42 | | elmapi 7879 |
. . . . . . . . . 10
|
43 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
44 | 43 | ex 450 |
. . . . . . . . . 10
|
45 | 16, 42, 44 | 3syl 18 |
. . . . . . . . 9
|
46 | 45 | imp 445 |
. . . . . . . 8
|
47 | 46 | ad2ant2r 783 |
. . . . . . 7
|
48 | 3, 4 | ringcl 18561 |
. . . . . . 7
|
49 | 30, 41, 47, 48 | syl3anc 1326 |
. . . . . 6
|
50 | 3, 4 | ringcl 18561 |
. . . . . 6
|
51 | 30, 36, 49, 50 | syl3anc 1326 |
. . . . 5
|
52 | 3, 28, 29, 29, 51 | gsumcom3fi 20206 |
. . . 4
g g g g |
53 | 5 | ad2antrr 762 |
. . . . . . . . 9
|
54 | 6 | ad2antrr 762 |
. . . . . . . . 9
|
55 | 11 | ad2antrr 762 |
. . . . . . . . 9
|
56 | 13 | ad2antrr 762 |
. . . . . . . . 9
|
57 | | simplr 792 |
. . . . . . . . 9
|
58 | | simpr 477 |
. . . . . . . . 9
|
59 | 7, 3, 4, 53, 54, 54, 54, 55, 56, 57, 58 | mamufv 20193 |
. . . . . . . 8
g |
60 | 59 | oveq1d 6665 |
. . . . . . 7
g |
61 | | eqid 2622 |
. . . . . . . 8
|
62 | | eqid 2622 |
. . . . . . . 8
|
63 | 46 | adantlr 751 |
. . . . . . . 8
|
64 | 5 | adantr 481 |
. . . . . . . . . 10
|
65 | 64 | ad2antrr 762 |
. . . . . . . . 9
|
66 | 32 | ad2antrr 762 |
. . . . . . . . . . 11
|
67 | | simplr 792 |
. . . . . . . . . . 11
|
68 | | simpr 477 |
. . . . . . . . . . 11
|
69 | 66, 67, 68 | fovrnd 6806 |
. . . . . . . . . 10
|
70 | 69 | adantlr 751 |
. . . . . . . . 9
|
71 | 38 | adantr 481 |
. . . . . . . . . . 11
|
72 | 71 | ad2antrr 762 |
. . . . . . . . . 10
|
73 | | simpr 477 |
. . . . . . . . . 10
|
74 | | simplr 792 |
. . . . . . . . . 10
|
75 | 72, 73, 74 | fovrnd 6806 |
. . . . . . . . 9
|
76 | 3, 4 | ringcl 18561 |
. . . . . . . . 9
|
77 | 65, 70, 75, 76 | syl3anc 1326 |
. . . . . . . 8
|
78 | | eqid 2622 |
. . . . . . . . 9
|
79 | | ovexd 6680 |
. . . . . . . . 9
|
80 | | fvexd 6203 |
. . . . . . . . 9
|
81 | 78, 54, 79, 80 | fsuppmptdm 8286 |
. . . . . . . 8
finSupp |
82 | 3, 61, 62, 4, 53, 54, 63, 77, 81 | gsummulc1 18606 |
. . . . . . 7
g g |
83 | 3, 4 | ringass 18564 |
. . . . . . . . . . 11
|
84 | 30, 36, 41, 47, 83 | syl13anc 1328 |
. . . . . . . . . 10
|
85 | 84 | anassrs 680 |
. . . . . . . . 9
|
86 | 85 | mpteq2dva 4744 |
. . . . . . . 8
|
87 | 86 | oveq2d 6666 |
. . . . . . 7
g g |
88 | 60, 82, 87 | 3eqtr2d 2662 |
. . . . . 6
g |
89 | 88 | mpteq2dva 4744 |
. . . . 5
g |
90 | 89 | oveq2d 6666 |
. . . 4
g
g g |
91 | 5 | ad2antrr 762 |
. . . . . . . . 9
|
92 | 6 | ad2antrr 762 |
. . . . . . . . 9
|
93 | 12 | ad2antrr 762 |
. . . . . . . . 9
|
94 | 16 | ad2antrr 762 |
. . . . . . . . 9
|
95 | 1, 2, 3, 4, 91, 92, 93, 94, 68 | mavmulfv 20352 |
. . . . . . . 8
g |
96 | 95 | oveq2d 6666 |
. . . . . . 7
g |
97 | 64 | ad2antrr 762 |
. . . . . . . . 9
|
98 | 71 | ad2antrr 762 |
. . . . . . . . . 10
|
99 | | simplr 792 |
. . . . . . . . . 10
|
100 | | simpr 477 |
. . . . . . . . . 10
|
101 | 98, 99, 100 | fovrnd 6806 |
. . . . . . . . 9
|
102 | 45 | ad2antrr 762 |
. . . . . . . . . 10
|
103 | 102 | imp 445 |
. . . . . . . . 9
|
104 | 97, 101, 103, 48 | syl3anc 1326 |
. . . . . . . 8
|
105 | | eqid 2622 |
. . . . . . . . 9
|
106 | | ovexd 6680 |
. . . . . . . . 9
|
107 | | fvexd 6203 |
. . . . . . . . 9
|
108 | 105, 92, 106, 107 | fsuppmptdm 8286 |
. . . . . . . 8
finSupp |
109 | 3, 61, 62, 4, 91, 92, 69, 104, 108 | gsummulc2 18607 |
. . . . . . 7
g g |
110 | 96, 109 | eqtr4d 2659 |
. . . . . 6
g |
111 | 110 | mpteq2dva 4744 |
. . . . 5
g |
112 | 111 | oveq2d 6666 |
. . . 4
g g g |
113 | 52, 90, 112 | 3eqtr4d 2666 |
. . 3
g
g |
114 | 15 | adantr 481 |
. . . 4
|
115 | 16 | adantr 481 |
. . . 4
|
116 | | simpr 477 |
. . . 4
|
117 | 1, 2, 3, 4, 64, 29, 114, 115, 116 | mavmulfv 20352 |
. . 3
g |
118 | 8 | adantr 481 |
. . . 4
|
119 | 21 | adantr 481 |
. . . 4
|
120 | 1, 2, 3, 4, 64, 29, 118, 119, 116 | mavmulfv 20352 |
. . 3
g |
121 | 113, 117,
120 | 3eqtr4d 2666 |
. 2
|
122 | 20, 25, 121 | eqfnfvd 6314 |
1
|