Step | Hyp | Ref
| Expression |
1 | | jensen.7 |
. . . . . 6
 ℂfld g    |
2 | | jensen.5 |
. . . . . . . . 9
          |
3 | | ffn 5739 |
. . . . . . . . 9
       
  |
4 | 2, 3 | syl 17 |
. . . . . . . 8
   |
5 | | fnresdm 5695 |
. . . . . . . 8
     |
6 | 4, 5 | syl 17 |
. . . . . . 7
     |
7 | 6 | oveq2d 6324 |
. . . . . 6
 ℂfld g 
  ℂfld g    |
8 | 1, 7 | breqtrrd 4422 |
. . . . 5
 ℂfld g      |
9 | | ssid 3437 |
. . . . 5
 |
10 | 8, 9 | jctil 546 |
. . . 4
 
ℂfld g       |
11 | | jensen.4 |
. . . . 5
   |
12 | | sseq1 3439 |
. . . . . . . . 9


   |
13 | | reseq2 5106 |
. . . . . . . . . . . . 13

  
   |
14 | | res0 5115 |
. . . . . . . . . . . . 13
   |
15 | 13, 14 | syl6eq 2521 |
. . . . . . . . . . . 12

    |
16 | 15 | oveq2d 6324 |
. . . . . . . . . . 11

ℂfld g    ℂfld g    |
17 | | cnfld0 19069 |
. . . . . . . . . . . 12
  ℂfld |
18 | 17 | gsum0 16599 |
. . . . . . . . . . 11
ℂfld g 
 |
19 | 16, 18 | syl6eq 2521 |
. . . . . . . . . 10

ℂfld g      |
20 | 19 | breq2d 4407 |
. . . . . . . . 9

 ℂfld g 
     |
21 | 12, 20 | anbi12d 725 |
. . . . . . . 8

 
ℂfld g 
  

    |
22 | | reseq2 5106 |
. . . . . . . . . . 11

            |
23 | 22 | oveq2d 6324 |
. . . . . . . . . 10

ℂfld g   
   ℂfld g   
     |
24 | 23, 19 | oveq12d 6326 |
. . . . . . . . 9

 ℂfld g       ℂfld g      ℂfld g   
      |
25 | | reseq2 5106 |
. . . . . . . . . . . . 13

                |
26 | 25 | oveq2d 6324 |
. . . . . . . . . . . 12

ℂfld g   
     ℂfld g   
       |
27 | 26, 19 | oveq12d 6326 |
. . . . . . . . . . 11

 ℂfld g         ℂfld g      ℂfld g   
        |
28 | 27 | breq2d 4407 |
. . . . . . . . . 10

      ℂfld g   
     ℂfld g 
  
     ℂfld g             |
29 | 28 | rabbidv 3022 |
. . . . . . . . 9


     ℂfld g   
     ℂfld g 
    
     ℂfld g             |
30 | 24, 29 | eleq12d 2543 |
. . . . . . . 8

  ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
   
 ℂfld g   
    
     ℂfld g   
          |
31 | 21, 30 | imbi12d 327 |
. . . . . . 7

  
ℂfld g      ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
      

 ℂfld g   
    
     ℂfld g   
           |
32 | 31 | imbi2d 323 |
. . . . . 6

    ℂfld g 
    ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
        
  ℂfld g   
    
     ℂfld g   
            |
33 | | sseq1 3439 |
. . . . . . . . 9
 
   |
34 | | reseq2 5106 |
. . . . . . . . . . 11
       |
35 | 34 | oveq2d 6324 |
. . . . . . . . . 10
 ℂfld g    ℂfld g      |
36 | 35 | breq2d 4407 |
. . . . . . . . 9
 
ℂfld
g   
ℂfld g       |
37 | 33, 36 | anbi12d 725 |
. . . . . . . 8
  
ℂfld g    
 ℂfld g 
      |
38 | | reseq2 5106 |
. . . . . . . . . . 11
             |
39 | 38 | oveq2d 6324 |
. . . . . . . . . 10
 ℂfld g   
   ℂfld g   
     |
40 | 39, 35 | oveq12d 6326 |
. . . . . . . . 9
  ℂfld g       ℂfld g 
    ℂfld g   
   ℂfld g 
     |
41 | | reseq2 5106 |
. . . . . . . . . . . . 13
                 |
42 | 41 | oveq2d 6324 |
. . . . . . . . . . . 12
 ℂfld g   
     ℂfld g   
       |
43 | 42, 35 | oveq12d 6326 |
. . . . . . . . . . 11
  ℂfld g         ℂfld g 
    ℂfld g   
     ℂfld g 
     |
44 | 43 | breq2d 4407 |
. . . . . . . . . 10
     
 ℂfld g   
     ℂfld g 
  
     ℂfld g         ℂfld g 
      |
45 | 44 | rabbidv 3022 |
. . . . . . . . 9
 
     ℂfld g   
     ℂfld g 
    
     ℂfld g         ℂfld g 
      |
46 | 40, 45 | eleq12d 2543 |
. . . . . . . 8
   ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
   
 ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
       |
47 | 37, 46 | imbi12d 327 |
. . . . . . 7
    ℂfld g      ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
       ℂfld g      ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
        |
48 | 47 | imbi2d 323 |
. . . . . 6
  
 
ℂfld g 
    ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
        
ℂfld g      ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
         |
49 | | sseq1 3439 |
. . . . . . . . 9
             |
50 | | reseq2 5106 |
. . . . . . . . . . 11
       
       |
51 | 50 | oveq2d 6324 |
. . . . . . . . . 10
     ℂfld g 
  ℂfld g          |
52 | 51 | breq2d 4407 |
. . . . . . . . 9
      ℂfld g 
  ℂfld g           |
53 | 49, 52 | anbi12d 725 |
. . . . . . . 8
       ℂfld g 
  
    
ℂfld g            |
54 | | reseq2 5106 |
. . . . . . . . . . 11
            
        |
55 | 54 | oveq2d 6324 |
. . . . . . . . . 10
     ℂfld g   
   ℂfld g   
         |
56 | 55, 51 | oveq12d 6326 |
. . . . . . . . 9
      ℂfld g   
   ℂfld g 
    ℂfld g   
       ℂfld g           |
57 | | reseq2 5106 |
. . . . . . . . . . . . 13
        
     
          |
58 | 57 | oveq2d 6324 |
. . . . . . . . . . . 12
     ℂfld g   
     ℂfld g   
           |
59 | 58, 51 | oveq12d 6326 |
. . . . . . . . . . 11
      ℂfld g   
     ℂfld g 
    ℂfld g   
         ℂfld g           |
60 | 59 | breq2d 4407 |
. . . . . . . . . 10
           ℂfld g   
     ℂfld g 
  
     ℂfld g             ℂfld g            |
61 | 60 | rabbidv 3022 |
. . . . . . . . 9
           ℂfld g   
     ℂfld g 
    
     ℂfld g             ℂfld g            |
62 | 56, 61 | eleq12d 2543 |
. . . . . . . 8
       ℂfld g       ℂfld g           ℂfld g         ℂfld g 
   
 ℂfld g   
       ℂfld g         
     ℂfld g   
         ℂfld g             |
63 | 53, 62 | imbi12d 327 |
. . . . . . 7
       
ℂfld g 
    ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
          
ℂfld g 
        ℂfld g   
       ℂfld g         
     ℂfld g   
         ℂfld g              |
64 | 63 | imbi2d 323 |
. . . . . 6
         ℂfld g      ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
             ℂfld g 
        ℂfld g   
       ℂfld g         
     ℂfld g   
         ℂfld g               |
65 | | sseq1 3439 |
. . . . . . . . 9
 
   |
66 | | reseq2 5106 |
. . . . . . . . . . 11
       |
67 | 66 | oveq2d 6324 |
. . . . . . . . . 10
 ℂfld g    ℂfld g      |
68 | 67 | breq2d 4407 |
. . . . . . . . 9
 
ℂfld
g   
ℂfld g       |
69 | 65, 68 | anbi12d 725 |
. . . . . . . 8
  
ℂfld g    
 ℂfld g 
      |
70 | | reseq2 5106 |
. . . . . . . . . . 11
             |
71 | 70 | oveq2d 6324 |
. . . . . . . . . 10
 ℂfld g   
   ℂfld g   
     |
72 | 71, 67 | oveq12d 6326 |
. . . . . . . . 9
  ℂfld g       ℂfld g 
    ℂfld g   
   ℂfld g 
     |
73 | | reseq2 5106 |
. . . . . . . . . . . . 13
                 |
74 | 73 | oveq2d 6324 |
. . . . . . . . . . . 12
 ℂfld g   
     ℂfld g   
       |
75 | 74, 67 | oveq12d 6326 |
. . . . . . . . . . 11
  ℂfld g         ℂfld g 
    ℂfld g   
     ℂfld g 
     |
76 | 75 | breq2d 4407 |
. . . . . . . . . 10
     
 ℂfld g   
     ℂfld g 
  
     ℂfld g         ℂfld g 
      |
77 | 76 | rabbidv 3022 |
. . . . . . . . 9
 
     ℂfld g   
     ℂfld g 
    
     ℂfld g         ℂfld g 
      |
78 | 72, 77 | eleq12d 2543 |
. . . . . . . 8
   ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
   
 ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
       |
79 | 69, 78 | imbi12d 327 |
. . . . . . 7
    ℂfld g      ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
       ℂfld g      ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
        |
80 | 79 | imbi2d 323 |
. . . . . 6
  
 
ℂfld g 
    ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
        
ℂfld g      ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
         |
81 | | 0re 9661 |
. . . . . . . . . 10
 |
82 | 81 | ltnri 9761 |
. . . . . . . . 9
 |
83 | 82 | pm2.21i 136 |
. . . . . . . 8
  ℂfld g        
     ℂfld g   
         |
84 | 83 | adantl 473 |
. . . . . . 7
    ℂfld g        
     ℂfld g   
         |
85 | 84 | a1i 11 |
. . . . . 6
  

 ℂfld g   
    
     ℂfld g   
          |
86 | | impexp 453 |
. . . . . . . . . . . 12
  
ℂfld g      ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
       ℂfld g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
        |
87 | | simprl 772 |
. . . . . . . . . . . . . 14
  
      ℂfld g 
       
      |
88 | 87 | unssad 3602 |
. . . . . . . . . . . . 13
  
      ℂfld g 
       
  |
89 | | simpr 468 |
. . . . . . . . . . . . . . 15
   

    
ℂfld g          ℂfld g 
   ℂfld g 
    |
90 | | jensen.1 |
. . . . . . . . . . . . . . . . . . 19

  |
91 | 90 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
  |
92 | | jensen.2 |
. . . . . . . . . . . . . . . . . . 19
       |
93 | 92 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
      |
94 | | simplll 776 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
  |
95 | | jensen.3 |
. . . . . . . . . . . . . . . . . . 19
 

    ![[,] [,]](_icc.gif) 
  |
96 | 94, 95 | sylan 479 |
. . . . . . . . . . . . . . . . . 18
          
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
           ![[,] [,]](_icc.gif) 
  |
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 744 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
ℂfld g    |
102 | | jensen.8 |
. . . . . . . . . . . . . . . . . . 19
 

  ![[,] [,]](_icc.gif)               
                  |
103 | 94, 102 | sylan 479 |
. . . . . . . . . . . . . . . . . 18
          
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
      
  ![[,] [,]](_icc.gif)               
                  |
104 | | simpllr 777 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
  |
105 | 87 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
      |
106 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
ℂfld g    ℂfld g     |
107 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
ℂfld g        ℂfld g 
       |
108 | | cnring 19067 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld  |
109 | | ringcmn 17889 |
. . . . . . . . . . . . . . . . . . . . . . 23
ℂfld ℂfld CMnd |
110 | 108, 109 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      ℂfld g 
       
ℂfld CMnd |
111 | 11 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
      ℂfld g 
       
  |
112 | | ssfi 7810 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
113 | 111, 88, 112 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      ℂfld g 
       
  |
114 | | rege0subm 19101 |
. . . . . . . . . . . . . . . . . . . . . . 23
   SubMnd ℂfld |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      ℂfld g 
       
   SubMnd ℂfld  |
116 | 2 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
      ℂfld g 
       
         |
117 | 116, 88 | fssresd 5762 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      ℂfld g 
       
           |
118 | | c0ex 9655 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
      ℂfld g 
       
  |
120 | 117, 113,
119 | fdmfifsupp 7911 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      ℂfld g 
       
  finSupp   |
121 | 17, 110, 113, 115, 117, 120 | gsumsubmcl 17630 |
. . . . . . . . . . . . . . . . . . . . 21
  
      ℂfld g 
       
ℂfld
g         |
122 | | elrege0 11764 |
. . . . . . . . . . . . . . . . . . . . . 22
 ℂfld g        ℂfld g 
  ℂfld g 
     |
123 | 122 | simplbi 467 |
. . . . . . . . . . . . . . . . . . . . 21
 ℂfld g       ℂfld g 
    |
124 | 121, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
  
      ℂfld g 
       
ℂfld
g      |
125 | 124 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
ℂfld
g      |
126 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
ℂfld g      |
127 | 125, 126 | elrpd 11361 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
ℂfld
g      |
128 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . 20
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
 ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
      |
129 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . 22
  ℂfld g   
   ℂfld g 
           ℂfld g   
   ℂfld g 
      |
130 | 129 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . 21
  ℂfld g   
   ℂfld g 
       
 ℂfld g   
     ℂfld g 
  
    ℂfld g   
   ℂfld g 
     ℂfld g   
     ℂfld g 
      |
131 | 130 | elrab 3184 |
. . . . . . . . . . . . . . . . . . . 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 201 |
. . . . . . . . . . . . . . . . . . 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 466 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
 ℂfld g   
   ℂfld g 
     |
134 | 132 | simprd 470 |
. . . . . . . . . . . . . . . . . 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 23992 |
. . . . . . . . . . . . . . . . 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 5879 |
. . . . . . . . . . . . . . . . . . 19
  ℂfld g   
       ℂfld g        
        ℂfld g           ℂfld g 
          |
137 | 136 | breq1d 4405 |
. . . . . . . . . . . . . . . . . 18
  ℂfld g   
       ℂfld g        
      ℂfld g   
         ℂfld g             ℂfld g   
       ℂfld g           ℂfld g             ℂfld g            |
138 | 137 | elrab 3184 |
. . . . . . . . . . . . . . . . 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 217 |
. . . . . . . . . . . . . . . 16
   

    
ℂfld g          
ℂfld
g     ℂfld g       ℂfld g 
       
 ℂfld g   
     ℂfld g 
     
 ℂfld g   
       ℂfld g         
     ℂfld g   
         ℂfld g            |
140 | 139 | expr 626 |
. . . . . . . . . . . . . . 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 55 |
. . . . . . . . . . . . . 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 19051 |
. . . . . . . . . . . . . . . . . . . . 21
  ℂfld |
143 | | ringmnd 17867 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld ℂfld   |
144 | 108, 143 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
  
ℂfld   |
145 | | ssfi 7810 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
146 | 111, 87, 145 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      ℂfld g 
       
      |
147 | 146 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
         |
148 | | ssun2 3589 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
149 | | ssnid 3989 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
150 | 148, 149 | sselii 3415 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
         |
152 | | remulcl 9642 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
153 | 152 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
154 | | rge0ssre 11766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    |
155 | | fss 5749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
156 | 2, 154, 155 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
157 | 99, 90 | fssd 5750 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
158 | | inidm 3632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
159 | 153, 156,
157, 11, 11, 158 | off 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
160 | | ax-resscn 9614 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
161 | | fss 5749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
162 | 159, 160,
161 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . 23
          |
163 | 162 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . 22
   

    
ℂfld g          ℂfld g 
            |
164 | 87 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
   

    
ℂfld g          ℂfld g 
         |
165 | 163, 164 | fssresd 5762 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
                      |
166 | 2 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

    
ℂfld g          ℂfld g 
            |
167 | 111 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

    
ℂfld g          ℂfld g 
     |
168 | | fex 6155 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
   |
169 | 166, 167,
168 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

    
ℂfld g          ℂfld g 
     |
170 | 99 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

    
ℂfld g          ℂfld g 
         |
171 | | fex 6155 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
   |
172 | 170, 167,
171 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

    
ℂfld g          ℂfld g 
     |
173 | | offres 6807 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   
                       |
174 | 169, 172,
173 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

    
ℂfld g          ℂfld g 
                             |
175 | 174 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
   

    
ℂfld g          ℂfld g 
      
      supp                  supp    |
176 | 154, 160 | sstri 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    |
177 | | fss 5749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
178 | 166, 176,
177 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

    
ℂfld g          ℂfld g 
         |
179 | 178, 164 | fssresd 5762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

    
ℂfld g          ℂfld g 
                   |
180 | | eldifi 3544 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
181 | 180 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
ℂfld g          ℂfld g 
                  |
182 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                     |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
ℂfld g          ℂfld g 
                            |
184 | | difun2 3838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
185 | | difss 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
 |
186 | 184, 185 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
187 | 186 | sseli 3414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
188 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   

    
ℂfld g          ℂfld g 
   ℂfld g 
    |
189 | 88 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   

    
ℂfld g          ℂfld g 
     |
190 | 166, 189 | feqresmpt 5933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   

    
ℂfld g          ℂfld g 
             |
191 | 190 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   

    
ℂfld g          ℂfld g 
   ℂfld g    ℂfld g          |
192 | 113 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   

    
ℂfld g          ℂfld g 
     |
193 | 189 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
          
ℂfld g          ℂfld g 
      |
194 | 166 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
          
ℂfld g          ℂfld g 
             |
195 | 193, 194 | syldan 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
          
ℂfld g          ℂfld g 
             |
196 | 176, 195 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
ℂfld g          ℂfld g 
          |
197 | 192, 196 | gsumfsum 19111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   

    
ℂfld g          ℂfld g 
   ℂfld g        
      |
198 | 188, 191,
197 | 3eqtrrd 2510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   

    
ℂfld g          ℂfld g 
   
      |
199 | | elrege0 11764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
            |
200 | 195, 199 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
ℂfld g          ℂfld g 
                |
201 | 200 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
ℂfld g          ℂfld g 
          |
202 | 200 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
ℂfld g          ℂfld g 
          |
203 | 192, 201,
202 | fsum00 13935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   

    
ℂfld g          ℂfld g 
        

       |
204 | 198, 203 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   

    
ℂfld g          ℂfld g 
   
      |
205 | 204 | r19.21bi 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
ℂfld g          ℂfld g 
          |
206 | 187, 205 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
ℂfld g          ℂfld g 
                  |
207 | 183, 206 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
ℂfld g          ℂfld g 
                        |
208 | 179, 207 | suppss 6964 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

    
ℂfld g          ℂfld g 
          supp 
    |
209 | | mul02 9829 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
210 | 209 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
ℂfld g          ℂfld g 
        |
211 | 90 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   

    
ℂfld g          ℂfld g 
     |
212 | 211, 160 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

    
ℂfld g          ℂfld g 
     |
213 | 170, 212 | fssd 5750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

    
ℂfld g          ℂfld g 
         |
214 | 213, 164 | fssresd 5762 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

    
ℂfld g          ℂfld g 
                   |
215 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

    
ℂfld g          ℂfld g 
     |
216 | 208, 210,
179, 214, 147, 215 | suppssof1 6967 |
. . . . . . . . . . . . . . . . . . . . . 22
   

    
ℂfld g          ℂfld g 
                   supp      |
217 | 175, 216 | eqsstrd 3452 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
      
      supp      |
218 | 142, 17, 144, 147, 151, 165, 217 | gsumpt 17672 |
. . . . . . . . . . . . . . . . . . . 20
   

    
ℂfld g          ℂfld g 
   ℂfld g   
                      |
219 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
220 | 151, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   

    
ℂfld g          ℂfld g 
      
           
      |
221 | 166, 3 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
     |
222 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
223 | 170, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
     |
224 | 164, 151 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
     |
225 | | fnfvof 6564 |
. . . . . . . . . . . . . . . . . . . . 21
  

     
                |
226 | 221, 223,
167, 224, 225 | syl22anc 1293 |
. . . . . . . . . . . . . . . . . . . 20
   

    
ℂfld g          ℂfld g 
                      |
227 | 218, 220,
226 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          ℂfld g 
   ℂfld g   
                   |
228 | 142, 17, 144, 147, 151, 179, 208 | gsumpt 17672 |
. . . . . . . . . . . . . . . . . . . 20
   

    
ℂfld g          ℂfld g 
   ℂfld g                    |
229 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
230 | 151, 229 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   

    
ℂfld g          ℂfld g 
                   |
231 | 228, 230 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          ℂfld g 
   ℂfld g              |
232 | 227, 231 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          ℂfld g 
    ℂfld g           ℂfld g                           |
233 | 213, 224 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          ℂfld g 
         |
234 | 178, 224 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          ℂfld g 
         |
235 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . 21
   

    
ℂfld g          ℂfld g 
   ℂfld g 
        |
236 | 235, 231 | breqtrd 4420 |
. . . . . . . . . . . . . . . . . . . 20
   

    
ℂfld g          ℂfld g 
         |
237 | 236 | gt0ne0d 10199 |
. . . . . . . . . . . . . . . . . . 19
   

    
ℂfld g          ℂfld g 
         |
238 | 233, 234,
237 | divcan3d 10410 |
. . . . . . . . . . . . . . . . . 18
   

    
ℂfld g          ℂfld g 
                         |
239 | 232, 238 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
   

    
ℂfld g          ℂfld g 
    ℂfld g           ℂfld g               |
240 | 170, 224 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . 17
    ![]() |