Step | Hyp | Ref
| Expression |
1 | | mamucl.b |
. . . . . 6
|
2 | | mamudir.p |
. . . . . 6
|
3 | | mamucl.r |
. . . . . . . 8
|
4 | | ringcmn 18581 |
. . . . . . . 8
CMnd |
5 | 3, 4 | syl 17 |
. . . . . . 7
CMnd |
6 | 5 | adantr 481 |
. . . . . 6
CMnd |
7 | | mamudi.n |
. . . . . . 7
|
8 | 7 | adantr 481 |
. . . . . 6
|
9 | 3 | ad2antrr 762 |
. . . . . . 7
|
10 | | mamudir.x |
. . . . . . . . . 10
|
11 | | elmapi 7879 |
. . . . . . . . . 10
|
12 | 10, 11 | syl 17 |
. . . . . . . . 9
|
13 | 12 | ad2antrr 762 |
. . . . . . . 8
|
14 | | simplrl 800 |
. . . . . . . 8
|
15 | | simpr 477 |
. . . . . . . 8
|
16 | 13, 14, 15 | fovrnd 6806 |
. . . . . . 7
|
17 | | mamudir.y |
. . . . . . . . . 10
|
18 | | elmapi 7879 |
. . . . . . . . . 10
|
19 | 17, 18 | syl 17 |
. . . . . . . . 9
|
20 | 19 | ad2antrr 762 |
. . . . . . . 8
|
21 | | simplrr 801 |
. . . . . . . 8
|
22 | 20, 15, 21 | fovrnd 6806 |
. . . . . . 7
|
23 | | eqid 2622 |
. . . . . . . 8
|
24 | 1, 23 | ringcl 18561 |
. . . . . . 7
|
25 | 9, 16, 22, 24 | syl3anc 1326 |
. . . . . 6
|
26 | | mamudir.z |
. . . . . . . . . 10
|
27 | | elmapi 7879 |
. . . . . . . . . 10
|
28 | 26, 27 | syl 17 |
. . . . . . . . 9
|
29 | 28 | ad2antrr 762 |
. . . . . . . 8
|
30 | 29, 15, 21 | fovrnd 6806 |
. . . . . . 7
|
31 | 1, 23 | ringcl 18561 |
. . . . . . 7
|
32 | 9, 16, 30, 31 | syl3anc 1326 |
. . . . . 6
|
33 | | eqid 2622 |
. . . . . 6
|
34 | | eqid 2622 |
. . . . . 6
|
35 | 1, 2, 6, 8, 25, 32, 33, 34 | gsummptfidmadd2 18326 |
. . . . 5
g g
g |
36 | | ffn 6045 |
. . . . . . . . . . . . 13
|
37 | 20, 36 | syl 17 |
. . . . . . . . . . . 12
|
38 | | ffn 6045 |
. . . . . . . . . . . . 13
|
39 | 29, 38 | syl 17 |
. . . . . . . . . . . 12
|
40 | | mamudi.o |
. . . . . . . . . . . . . 14
|
41 | | xpfi 8231 |
. . . . . . . . . . . . . 14
|
42 | 7, 40, 41 | syl2anc 693 |
. . . . . . . . . . . . 13
|
43 | 42 | ad2antrr 762 |
. . . . . . . . . . . 12
|
44 | | opelxpi 5148 |
. . . . . . . . . . . . . . 15
|
45 | 44 | ancoms 469 |
. . . . . . . . . . . . . 14
|
46 | 45 | adantll 750 |
. . . . . . . . . . . . 13
|
47 | 46 | adantll 750 |
. . . . . . . . . . . 12
|
48 | | fnfvof 6911 |
. . . . . . . . . . . 12
|
49 | 37, 39, 43, 47, 48 | syl22anc 1327 |
. . . . . . . . . . 11
|
50 | | df-ov 6653 |
. . . . . . . . . . 11
|
51 | | df-ov 6653 |
. . . . . . . . . . . 12
|
52 | | df-ov 6653 |
. . . . . . . . . . . 12
|
53 | 51, 52 | oveq12i 6662 |
. . . . . . . . . . 11
|
54 | 49, 50, 53 | 3eqtr4g 2681 |
. . . . . . . . . 10
|
55 | 54 | oveq2d 6666 |
. . . . . . . . 9
|
56 | 1, 2, 23 | ringdi 18566 |
. . . . . . . . . 10
|
57 | 9, 16, 22, 30, 56 | syl13anc 1328 |
. . . . . . . . 9
|
58 | 55, 57 | eqtrd 2656 |
. . . . . . . 8
|
59 | 58 | mpteq2dva 4744 |
. . . . . . 7
|
60 | | eqidd 2623 |
. . . . . . . 8
|
61 | | eqidd 2623 |
. . . . . . . 8
|
62 | 8, 25, 32, 60, 61 | offval2 6914 |
. . . . . . 7
|
63 | 59, 62 | eqtr4d 2659 |
. . . . . 6
|
64 | 63 | oveq2d 6666 |
. . . . 5
g g |
65 | | mamudi.f |
. . . . . . 7
maMul
|
66 | 3 | adantr 481 |
. . . . . . 7
|
67 | | mamudi.m |
. . . . . . . 8
|
68 | 67 | adantr 481 |
. . . . . . 7
|
69 | 40 | adantr 481 |
. . . . . . 7
|
70 | 10 | adantr 481 |
. . . . . . 7
|
71 | 17 | adantr 481 |
. . . . . . 7
|
72 | | simprl 794 |
. . . . . . 7
|
73 | | simprr 796 |
. . . . . . 7
|
74 | 65, 1, 23, 66, 68, 8, 69, 70, 71, 72, 73 | mamufv 20193 |
. . . . . 6
g |
75 | 26 | adantr 481 |
. . . . . . 7
|
76 | 65, 1, 23, 66, 68, 8, 69, 70, 75, 72, 73 | mamufv 20193 |
. . . . . 6
g |
77 | 74, 76 | oveq12d 6668 |
. . . . 5
g
g |
78 | 35, 64, 77 | 3eqtr4d 2666 |
. . . 4
g |
79 | | ringmnd 18556 |
. . . . . . . 8
|
80 | 3, 79 | syl 17 |
. . . . . . 7
|
81 | 1, 2 | mndvcl 20197 |
. . . . . . 7
|
82 | 80, 17, 26, 81 | syl3anc 1326 |
. . . . . 6
|
83 | 82 | adantr 481 |
. . . . 5
|
84 | 65, 1, 23, 66, 68, 8, 69, 70, 83, 72, 73 | mamufv 20193 |
. . . 4
g |
85 | 1, 3, 65, 67, 7, 40, 10, 17 | mamucl 20207 |
. . . . . . . 8
|
86 | | elmapi 7879 |
. . . . . . . 8
|
87 | | ffn 6045 |
. . . . . . . 8
|
88 | 85, 86, 87 | 3syl 18 |
. . . . . . 7
|
89 | 88 | adantr 481 |
. . . . . 6
|
90 | 1, 3, 65, 67, 7, 40, 10, 26 | mamucl 20207 |
. . . . . . . 8
|
91 | | elmapi 7879 |
. . . . . . . 8
|
92 | | ffn 6045 |
. . . . . . . 8
|
93 | 90, 91, 92 | 3syl 18 |
. . . . . . 7
|
94 | 93 | adantr 481 |
. . . . . 6
|
95 | | xpfi 8231 |
. . . . . . . 8
|
96 | 67, 40, 95 | syl2anc 693 |
. . . . . . 7
|
97 | 96 | adantr 481 |
. . . . . 6
|
98 | | opelxpi 5148 |
. . . . . . 7
|
99 | 98 | adantl 482 |
. . . . . 6
|
100 | | fnfvof 6911 |
. . . . . 6
|
101 | 89, 94, 97, 99, 100 | syl22anc 1327 |
. . . . 5
|
102 | | df-ov 6653 |
. . . . 5
|
103 | | df-ov 6653 |
. . . . . 6
|
104 | | df-ov 6653 |
. . . . . 6
|
105 | 103, 104 | oveq12i 6662 |
. . . . 5
|
106 | 101, 102,
105 | 3eqtr4g 2681 |
. . . 4
|
107 | 78, 84, 106 | 3eqtr4d 2666 |
. . 3
|
108 | 107 | ralrimivva 2971 |
. 2
|
109 | 1, 3, 65, 67, 7, 40, 10, 82 | mamucl 20207 |
. . . 4
|
110 | | elmapi 7879 |
. . . 4
|
111 | | ffn 6045 |
. . . 4
|
112 | 109, 110,
111 | 3syl 18 |
. . 3
|
113 | 1, 2 | mndvcl 20197 |
. . . . 5
|
114 | 80, 85, 90, 113 | syl3anc 1326 |
. . . 4
|
115 | | elmapi 7879 |
. . . 4
|
116 | | ffn 6045 |
. . . 4
|
117 | 114, 115,
116 | 3syl 18 |
. . 3
|
118 | | eqfnov2 6767 |
. . 3
|
119 | 112, 117,
118 | syl2anc 693 |
. 2
|
120 | 108, 119 | mpbird 247 |
1
|