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