Step | Hyp | Ref
| Expression |
1 | | jensen.7 |
. . . . . 6
ℂfld g |
2 | | jensen.5 |
. . . . . . . . 9
|
3 | | ffn 6045 |
. . . . . . . . 9
|
4 | 2, 3 | syl 17 |
. . . . . . . 8
|
5 | | fnresdm 6000 |
. . . . . . . 8
|
6 | 4, 5 | syl 17 |
. . . . . . 7
|
7 | 6 | oveq2d 6666 |
. . . . . 6
ℂfld g
ℂfld g |
8 | 1, 7 | breqtrrd 4681 |
. . . . 5
ℂfld g |
9 | | ssid 3624 |
. . . . 5
|
10 | 8, 9 | jctil 560 |
. . . 4
ℂfld g |
11 | | jensen.4 |
. . . . 5
|
12 | | sseq1 3626 |
. . . . . . . . 9
|
13 | | reseq2 5391 |
. . . . . . . . . . . . 13
|
14 | | res0 5400 |
. . . . . . . . . . . . 13
|
15 | 13, 14 | syl6eq 2672 |
. . . . . . . . . . . 12
|
16 | 15 | oveq2d 6666 |
. . . . . . . . . . 11
ℂfld g ℂfld g |
17 | | cnfld0 19770 |
. . . . . . . . . . . 12
ℂfld |
18 | 17 | gsum0 17278 |
. . . . . . . . . . 11
ℂfld g
|
19 | 16, 18 | syl6eq 2672 |
. . . . . . . . . 10
ℂfld g |
20 | 19 | breq2d 4665 |
. . . . . . . . 9
ℂfld g
|
21 | 12, 20 | anbi12d 747 |
. . . . . . . 8
ℂfld g
|
22 | | reseq2 5391 |
. . . . . . . . . . 11
|
23 | 22 | oveq2d 6666 |
. . . . . . . . . 10
ℂfld g
ℂfld g
|
24 | 23, 19 | oveq12d 6668 |
. . . . . . . . 9
ℂfld g ℂfld g ℂfld g
|
25 | | reseq2 5391 |
. . . . . . . . . . . . 13
|
26 | 25 | oveq2d 6666 |
. . . . . . . . . . . 12
ℂfld g
ℂfld g
|
27 | 26, 19 | oveq12d 6668 |
. . . . . . . . . . 11
ℂfld g ℂfld g ℂfld g
|
28 | 27 | breq2d 4665 |
. . . . . . . . . 10
ℂfld g
ℂfld g
ℂfld g |
29 | 28 | rabbidv 3189 |
. . . . . . . . 9
ℂfld g
ℂfld g
ℂfld g |
30 | 24, 29 | eleq12d 2695 |
. . . . . . . 8
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
31 | 21, 30 | imbi12d 334 |
. . . . . . 7
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
32 | 31 | imbi2d 330 |
. . . . . 6
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
33 | | sseq1 3626 |
. . . . . . . . 9
|
34 | | reseq2 5391 |
. . . . . . . . . . 11
|
35 | 34 | oveq2d 6666 |
. . . . . . . . . 10
ℂfld g ℂfld g |
36 | 35 | breq2d 4665 |
. . . . . . . . 9
ℂfld
g
ℂfld g |
37 | 33, 36 | anbi12d 747 |
. . . . . . . 8
ℂfld g
ℂfld g
|
38 | | reseq2 5391 |
. . . . . . . . . . 11
|
39 | 38 | oveq2d 6666 |
. . . . . . . . . 10
ℂfld g
ℂfld g
|
40 | 39, 35 | oveq12d 6668 |
. . . . . . . . 9
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
41 | | reseq2 5391 |
. . . . . . . . . . . . 13
|
42 | 41 | oveq2d 6666 |
. . . . . . . . . . . 12
ℂfld g
ℂfld g
|
43 | 42, 35 | oveq12d 6668 |
. . . . . . . . . . 11
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
44 | 43 | breq2d 4665 |
. . . . . . . . . 10
ℂfld g
ℂfld g
ℂfld g ℂfld g
|
45 | 44 | rabbidv 3189 |
. . . . . . . . 9
ℂfld g
ℂfld g
ℂfld g ℂfld g
|
46 | 40, 45 | eleq12d 2695 |
. . . . . . . 8
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
47 | 37, 46 | imbi12d 334 |
. . . . . . 7
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
48 | 47 | imbi2d 330 |
. . . . . 6
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
49 | | sseq1 3626 |
. . . . . . . . 9
|
50 | | reseq2 5391 |
. . . . . . . . . . 11
|
51 | 50 | oveq2d 6666 |
. . . . . . . . . 10
ℂfld g
ℂfld g |
52 | 51 | breq2d 4665 |
. . . . . . . . 9
ℂfld g
ℂfld g |
53 | 49, 52 | anbi12d 747 |
. . . . . . . 8
ℂfld g
ℂfld g |
54 | | reseq2 5391 |
. . . . . . . . . . 11
|
55 | 54 | oveq2d 6666 |
. . . . . . . . . 10
ℂfld g
ℂfld g
|
56 | 55, 51 | oveq12d 6668 |
. . . . . . . . 9
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
57 | | reseq2 5391 |
. . . . . . . . . . . . 13
|
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . 12
ℂfld g
ℂfld g
|
59 | 58, 51 | oveq12d 6668 |
. . . . . . . . . . 11
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
60 | 59 | breq2d 4665 |
. . . . . . . . . 10
ℂfld g
ℂfld g
ℂfld g ℂfld g |
61 | 60 | rabbidv 3189 |
. . . . . . . . 9
ℂfld g
ℂfld g
ℂfld g ℂfld g |
62 | 56, 61 | eleq12d 2695 |
. . . . . . . 8
ℂfld g ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
63 | 53, 62 | imbi12d 334 |
. . . . . . 7
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
64 | 63 | imbi2d 330 |
. . . . . 6
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
65 | | sseq1 3626 |
. . . . . . . . 9
|
66 | | reseq2 5391 |
. . . . . . . . . . 11
|
67 | 66 | oveq2d 6666 |
. . . . . . . . . 10
ℂfld g ℂfld g |
68 | 67 | breq2d 4665 |
. . . . . . . . 9
ℂfld
g
ℂfld g |
69 | 65, 68 | anbi12d 747 |
. . . . . . . 8
ℂfld g
ℂfld g
|
70 | | reseq2 5391 |
. . . . . . . . . . 11
|
71 | 70 | oveq2d 6666 |
. . . . . . . . . 10
ℂfld g
ℂfld g
|
72 | 71, 67 | oveq12d 6668 |
. . . . . . . . 9
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
73 | | reseq2 5391 |
. . . . . . . . . . . . 13
|
74 | 73 | oveq2d 6666 |
. . . . . . . . . . . 12
ℂfld g
ℂfld g
|
75 | 74, 67 | oveq12d 6668 |
. . . . . . . . . . 11
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
76 | 75 | breq2d 4665 |
. . . . . . . . . 10
ℂfld g
ℂfld g
ℂfld g ℂfld g
|
77 | 76 | rabbidv 3189 |
. . . . . . . . 9
ℂfld g
ℂfld g
ℂfld g ℂfld g
|
78 | 72, 77 | eleq12d 2695 |
. . . . . . . 8
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
79 | 69, 78 | imbi12d 334 |
. . . . . . 7
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
80 | 79 | imbi2d 330 |
. . . . . 6
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
81 | | 0re 10040 |
. . . . . . . . . 10
|
82 | 81 | ltnri 10146 |
. . . . . . . . 9
|
83 | 82 | pm2.21i 116 |
. . . . . . . 8
ℂfld g
ℂfld g
|
84 | 83 | adantl 482 |
. . . . . . 7
ℂfld g
ℂfld g
|
85 | 84 | a1i 11 |
. . . . . 6
ℂfld g
ℂfld g
|
86 | | impexp 462 |
. . . . . . . . . . . 12
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
87 | | simprl 794 |
. . . . . . . . . . . . . 14
ℂfld g
|
88 | 87 | unssad 3790 |
. . . . . . . . . . . . 13
ℂfld g
|
89 | | simpr 477 |
. . . . . . . . . . . . . . 15
ℂfld g ℂfld g
ℂfld g
|
90 | | jensen.1 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 90 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
92 | | jensen.2 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 92 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
94 | | simplll 798 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
95 | | jensen.3 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 94, 95 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
97 | 94, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
98 | 94, 2 | syl 17 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
99 | | jensen.6 |
. . . . . . . . . . . . . . . . . . 19
|
100 | 94, 99 | syl 17 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
101 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g |
102 | | jensen.8 |
. . . . . . . . . . . . . . . . . . 19
|
103 | 94, 102 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
104 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
105 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
106 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
ℂfld g ℂfld g |
107 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
ℂfld g ℂfld g
|
108 | | cnring 19768 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld |
109 | | ringcmn 18581 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld ℂfld CMnd |
110 | 108, 109 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g
ℂfld CMnd |
111 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g
|
112 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
113 | 111, 88, 112 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g
|
114 | | rege0subm 19802 |
. . . . . . . . . . . . . . . . . . . . . . 23
SubMndℂfld |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g
SubMndℂfld |
116 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g
|
117 | 116, 88 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g
|
118 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g
|
120 | 117, 113,
119 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g
finSupp |
121 | 17, 110, 113, 115, 117, 120 | gsumsubmcl 18319 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g
ℂfld
g |
122 | | elrege0 12278 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
ℂfld g
|
123 | 122 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
124 | 121, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g
ℂfld
g |
125 | 124 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld
g |
126 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g |
127 | 125, 126 | elrpd 11869 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld
g |
128 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
129 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
130 | 129 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
131 | 130 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
132 | 128, 131 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
133 | 132 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
134 | 132 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
135 | 91, 93, 96, 97, 98, 100, 101, 103, 104, 105, 106, 107, 127, 133, 134 | jensenlem2 24714 |
. . . . . . . . . . . . . . . . 17
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g |
136 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g
ℂfld g
ℂfld g ℂfld g
|
137 | 136 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g
ℂfld g ℂfld g ℂfld g |
138 | 137 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g |
139 | 135, 138 | sylibr 224 |
. . . . . . . . . . . . . . . 16
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
140 | 139 | expr 643 |
. . . . . . . . . . . . . . 15
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
141 | 89, 140 | embantd 59 |
. . . . . . . . . . . . . 14
ℂfld g ℂfld g
ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
142 | | cnfldbas 19750 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld |
143 | | ringmnd 18556 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld ℂfld |
144 | 108, 143 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
ℂfld |
145 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
146 | 111, 87, 145 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g
|
147 | 146 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
148 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
149 | | vsnid 4209 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
150 | 148, 149 | sselii 3600 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
152 | | remulcl 10021 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
153 | 152 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
154 | | rge0ssre 12280 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
155 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
156 | 2, 154, 155 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
157 | 99, 90 | fssd 6057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
158 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
159 | 153, 156,
157, 11, 11, 158 | off 6912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
160 | | ax-resscn 9993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
161 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
162 | 159, 160,
161 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
163 | 162 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
|
164 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
|
165 | 163, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
166 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
167 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
168 | | fex 6490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
169 | 166, 167,
168 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ℂfld g ℂfld g
|
170 | 99 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
171 | | fex 6490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
172 | 170, 167,
171 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ℂfld g ℂfld g
|
173 | | offres 7163 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
174 | 169, 172,
173 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g ℂfld g
|
175 | 174 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
supp supp |
176 | 154, 160 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
177 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
178 | 166, 176,
177 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
179 | 178, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ℂfld g ℂfld g
|
180 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
181 | 180 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
ℂfld g ℂfld g
|
182 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
184 | | difun2 4048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
185 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
186 | 184, 185 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
187 | 186 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
188 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℂfld g ℂfld g
ℂfld g
|
189 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
ℂfld g ℂfld g
|
190 | 166, 189 | feqresmpt 6250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ℂfld g ℂfld g
|
191 | 190 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℂfld g ℂfld g
ℂfld g ℂfld g |
192 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ℂfld g ℂfld g
|
193 | 189 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ℂfld g ℂfld g
|
194 | 166 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ℂfld g ℂfld g
|
195 | 193, 194 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
ℂfld g ℂfld g
|
196 | 176, 195 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ℂfld g ℂfld g
|
197 | 192, 196 | gsumfsum 19813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℂfld g ℂfld g
ℂfld g
|
198 | 188, 191,
197 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ℂfld g ℂfld g
|
199 | | elrege0 12278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
200 | 195, 199 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ℂfld g ℂfld g
|
201 | 200 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℂfld g ℂfld g
|
202 | 200 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℂfld g ℂfld g
|
203 | 192, 201,
202 | fsum00 14530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ℂfld g ℂfld g
|
204 | 198, 203 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
ℂfld g ℂfld g
|
205 | 204 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
ℂfld g ℂfld g
|
206 | 187, 205 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
207 | 183, 206 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ℂfld g ℂfld g
|
208 | 179, 207 | suppss 7325 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g ℂfld g
supp
|
209 | | mul02 10214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
210 | 209 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g ℂfld g
|
211 | 90 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
ℂfld g ℂfld g
|
212 | 211, 160 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
213 | 170, 212 | fssd 6057 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ℂfld g ℂfld g
|
214 | 213, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g ℂfld g
|
215 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g ℂfld g
|
216 | 208, 210,
179, 214, 147, 215 | suppssof1 7328 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
supp |
217 | 175, 216 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
supp |
218 | 142, 17, 144, 147, 151, 165, 217 | gsumpt 18361 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
ℂfld g
|
219 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . 21
|
220 | 151, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
|
221 | 166, 3 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
222 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
|
223 | 170, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
224 | 164, 151 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
225 | | fnfvof 6911 |
. . . . . . . . . . . . . . . . . . . . 21
|
226 | 221, 223,
167, 224, 225 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
|
227 | 218, 220,
226 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
ℂfld g
|
228 | 142, 17, 144, 147, 151, 179, 208 | gsumpt 18361 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
ℂfld g |
229 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . 21
|
230 | 151, 229 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
|
231 | 228, 230 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
ℂfld g |
232 | 227, 231 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
ℂfld g ℂfld g
ℂfld g ℂfld g |
233 | 213, 224 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
|
234 | 178, 224 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
|
235 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
ℂfld g
|
236 | 235, 231 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
|
237 | 236 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
|
238 | 233, 234,
237 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . 18
ℂfld g ℂfld g
|
239 | 232, 238 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
ℂfld g ℂfld g
ℂfld g ℂfld g |
240 | 170, 224 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
ℂfld g ℂfld g
|
241 | 239, 240 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
ℂfld g ℂfld g
ℂfld g ℂfld g |
242 | 92 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
|
243 | 242, 240 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
ℂfld g ℂfld g
|
244 | 243 | leidd 10594 |
. . . . . . . . . . . . . . . . 17
ℂfld g ℂfld g
|
245 | 239 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
ℂfld g ℂfld g
ℂfld g
ℂfld g |
246 | | fco 6058 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
247 | 92, 99, 246 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
248 | 153, 156,
247, 11, 11, 158 | off 6912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
249 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
250 | 248, 160,
249 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
251 | 250 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
|
252 | 251, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
253 | 247 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ℂfld g ℂfld g
|
254 | | fex 6490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
255 | 253, 167,
254 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ℂfld g ℂfld g
|
256 | | offres 7163 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
257 | 169, 255,
256 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g ℂfld g
|
258 | 257 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
supp supp |
259 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
260 | 253, 160,
259 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ℂfld g ℂfld g
|
261 | 260, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld g ℂfld g
|
262 | 208, 210,
179, 261, 147, 215 | suppssof1 7328 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
supp |
263 | 258, 262 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
supp |
264 | 142, 17, 144, 147, 151, 252, 263 | gsumpt 18361 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
ℂfld g
|
265 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . 21
|
266 | 151, 265 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
|
267 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
268 | 92, 267 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
269 | | fnfco 6069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
270 | 268, 99, 269 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
271 | 270 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
|
272 | | fnfvof 6911 |
. . . . . . . . . . . . . . . . . . . . . 22
|
273 | 221, 271,
167, 224, 272 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
274 | | fvco3 6275 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
275 | 170, 224,
274 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld g ℂfld g
|
276 | 275 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld g ℂfld g
|
277 | 273, 276 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld g ℂfld g
|
278 | 264, 266,
277 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
ℂfld g
|
279 | 278, 231 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
ℂfld g ℂfld g
ℂfld g ℂfld g |
280 | 243 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
ℂfld g ℂfld g
|
281 | 280, 234,
237 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . 18
ℂfld g ℂfld g
|
282 | 279, 281 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
ℂfld g ℂfld g
ℂfld g ℂfld g |
283 | 244, 245,
282 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
ℂfld g ℂfld g
ℂfld g
ℂfld g ℂfld g ℂfld g |
284 | 241, 283,
138 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
ℂfld g ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g |
285 | 284 | a1d 25 |
. . . . . . . . . . . . . 14
ℂfld g ℂfld g
ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
286 | 122 | simprbi 480 |
. . . . . . . . . . . . . . . 16
ℂfld g ℂfld g |
287 | 121, 286 | syl 17 |
. . . . . . . . . . . . . . 15
ℂfld g
ℂfld g |
288 | | leloe 10124 |
. . . . . . . . . . . . . . . 16
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
289 | 81, 124, 288 | sylancr 695 |
. . . . . . . . . . . . . . 15
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
290 | 287, 289 | mpbid 222 |
. . . . . . . . . . . . . 14
ℂfld g
ℂfld g
ℂfld g
|
291 | 141, 285,
290 | mpjaodan 827 |
. . . . . . . . . . . . 13
ℂfld g
ℂfld
g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
292 | 88, 291 | embantd 59 |
. . . . . . . . . . . 12
ℂfld g
ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
293 | 86, 292 | syl5bi 232 |
. . . . . . . . . . 11
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
294 | 293 | ex 450 |
. . . . . . . . . 10
ℂfld g
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
295 | 294 | com23 86 |
. . . . . . . . 9
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
296 | 295 | expcom 451 |
. . . . . . . 8
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
297 | 296 | adantl 482 |
. . . . . . 7
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
298 | 297 | a2d 29 |
. . . . . 6
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
299 | 32, 48, 64, 80, 85, 298 | findcard2s 8201 |
. . . . 5
ℂfld g
ℂfld g ℂfld g
ℂfld g
ℂfld g
|
300 | 11, 299 | mpcom 38 |
. . . 4
ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g
|
301 | 10, 300 | mpd 15 |
. . 3
ℂfld g
ℂfld g
ℂfld g
ℂfld g
|
302 | | ffn 6045 |
. . . . . . 7
|
303 | 159, 302 | syl 17 |
. . . . . 6
|
304 | | fnresdm 6000 |
. . . . . 6
|
305 | 303, 304 | syl 17 |
. . . . 5
|
306 | 305 | oveq2d 6666 |
. . . 4
ℂfld g
ℂfld g
|
307 | 306, 7 | oveq12d 6668 |
. . 3
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
308 | 4, 270, 11, 11, 158 | offn 6908 |
. . . . . . . 8
|
309 | | fnresdm 6000 |
. . . . . . . 8
|
310 | 308, 309 | syl 17 |
. . . . . . 7
|
311 | 310 | oveq2d 6666 |
. . . . . 6
ℂfld g
ℂfld g
|
312 | 311, 7 | oveq12d 6668 |
. . . . 5
ℂfld g
ℂfld g
ℂfld g
ℂfld g |
313 | 312 | breq2d 4665 |
. . . 4
ℂfld g ℂfld g
ℂfld g ℂfld g |
314 | 313 | rabbidv 3189 |
. . 3
ℂfld g ℂfld g
ℂfld g ℂfld g |
315 | 301, 307,
314 | 3eltr3d 2715 |
. 2
ℂfld g
ℂfld g
ℂfld g ℂfld g |
316 | | fveq2 6191 |
. . . 4
ℂfld g ℂfld g ℂfld g ℂfld g |
317 | 316 | breq1d 4663 |
. . 3
ℂfld g ℂfld g ℂfld g ℂfld g
ℂfld g
ℂfld g ℂfld g
ℂfld g |
318 | 317 | elrab 3363 |
. 2
ℂfld g
ℂfld g
ℂfld g ℂfld g ℂfld g ℂfld g ℂfld g ℂfld g ℂfld g ℂfld g |
319 | 315, 318 | sylib 208 |
1
ℂfld g ℂfld g ℂfld g ℂfld g ℂfld g ℂfld g |