Step | Hyp | Ref
| Expression |
1 | | tchcph.1 |
. . . 4
   |
2 | | tchval.n |
. . . . 5
toCHil   |
3 | 2 | tchphl 22201 |
. . . 4
   |
4 | 1, 3 | sylib 200 |
. . 3
   |
5 | | tchcph.v |
. . . . . . 7
     |
6 | | tchcph.h |
. . . . . . 7
     |
7 | 2, 5, 6 | tchval 22192 |
. . . . . 6
 toNrmGrp

         |
8 | | eqid 2451 |
. . . . . 6
         |
9 | | eqid 2451 |
. . . . . 6
         |
10 | | phllmod 19197 |
. . . . . . . 8
   |
11 | 1, 10 | syl 17 |
. . . . . . 7
   |
12 | | lmodgrp 18098 |
. . . . . . 7

  |
13 | 11, 12 | syl 17 |
. . . . . 6
   |
14 | | tchcph.f |
. . . . . . . . 9
Scalar   |
15 | | tchcph.2 |
. . . . . . . . 9
 ℂfld
↾s    |
16 | 2, 5, 14, 1, 15, 6 | tchcphlem3 22207 |
. . . . . . . 8
 
 
   |
17 | | tchcph.4 |
. . . . . . . 8
 
     |
18 | 16, 17 | resqrtcld 13479 |
. . . . . . 7
 
         |
19 | | eqid 2451 |
. . . . . . 7
            
    |
20 | 18, 19 | fmptd 6046 |
. . . . . 6
     
         |
21 | | oveq12 6299 |
. . . . . . . . . . . 12
 
       |
22 | 21 | anidms 651 |
. . . . . . . . . . 11
 
     |
23 | 22 | fveq2d 5869 |
. . . . . . . . . 10
          
    |
24 | | fvex 5875 |
. . . . . . . . . 10
       |
25 | 23, 19, 24 | fvmpt3i 5953 |
. . . . . . . . 9
      
              |
26 | 25 | adantl 468 |
. . . . . . . 8
 
      
              |
27 | 26 | eqeq1d 2453 |
. . . . . . 7
 
       
               |
28 | | eqid 2451 |
. . . . . . . . . . . . . . 15
         |
29 | | phllvec 19196 |
. . . . . . . . . . . . . . . . 17
   |
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
31 | 14 | lvecdrng 18328 |
. . . . . . . . . . . . . . . 16

  |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
   |
33 | 28, 15, 32 | cphsubrglem 22155 |
. . . . . . . . . . . . . 14
  ℂfld ↾s                SubRing ℂfld   |
34 | 33 | simp2d 1021 |
. . . . . . . . . . . . 13
         |
35 | | inss2 3653 |
. . . . . . . . . . . . 13
   |
36 | 34, 35 | syl6eqss 3482 |
. . . . . . . . . . . 12
    
  |
37 | 36 | adantr 467 |
. . . . . . . . . . 11
 
       |
38 | 14, 6, 5, 28 | ipcl 19200 |
. . . . . . . . . . . . 13
 
 
       |
39 | 38 | 3anidm23 1327 |
. . . . . . . . . . . 12
   
       |
40 | 1, 39 | sylan 474 |
. . . . . . . . . . 11
 
 
       |
41 | 37, 40 | sseldd 3433 |
. . . . . . . . . 10
 
 
   |
42 | 41 | sqrtcld 13499 |
. . . . . . . . 9
 
         |
43 | | sqeq0 12339 |
. . . . . . . . 9
            
    
         |
44 | 42, 43 | syl 17 |
. . . . . . . 8
 
      
    
         |
45 | 41 | sqsqrtd 13501 |
. . . . . . . . 9
 
     
         |
46 | 2, 5, 14, 1, 15 | tchclm 22206 |
. . . . . . . . . . 11
 CMod |
47 | 14 | clm0 22103 |
. . . . . . . . . . 11
 CMod       |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
       |
49 | 48 | adantr 467 |
. . . . . . . . 9
 
       |
50 | 45, 49 | eqeq12d 2466 |
. . . . . . . 8
 
      
    
         |
51 | 44, 50 | bitr3d 259 |
. . . . . . 7
 
     
  
        |
52 | | eqid 2451 |
. . . . . . . . 9
         |
53 | 14, 6, 5, 52, 9 | ipeq0 19205 |
. . . . . . . 8
         
       |
54 | 1, 53 | sylan 474 |
. . . . . . 7
 
       
       |
55 | 27, 51, 54 | 3bitrd 283 |
. . . . . 6
 
       
             |
56 | 1 | adantr 467 |
. . . . . . . 8
 

 
  |
57 | 33 | simp1d 1020 |
. . . . . . . . 9
 ℂfld
↾s        |
58 | 57 | adantr 467 |
. . . . . . . 8
 

 
ℂfld
↾s        |
59 | | 3anass 989 |
. . . . . . . . . . 11
      
    
     |
60 | | tchcph.3 |
. . . . . . . . . . . . . 14
 

        |
61 | | simpr2 1015 |
. . . . . . . . . . . . . . . 16
 

 
  |
62 | 61 | recnd 9669 |
. . . . . . . . . . . . . . 15
 

 
  |
63 | 62 | sqrtcld 13499 |
. . . . . . . . . . . . . 14
 

        |
64 | 60, 63 | jca 535 |
. . . . . . . . . . . . 13
 

              |
65 | 64 | ex 436 |
. . . . . . . . . . . 12
                 |
66 | 34 | eleq2d 2514 |
. . . . . . . . . . . . . . . . 17
           |
67 | | recn 9629 |
. . . . . . . . . . . . . . . . . 18
   |
68 | | elin 3617 |
. . . . . . . . . . . . . . . . . . 19
       |
69 | 68 | rbaib 917 |
. . . . . . . . . . . . . . . . . 18
   
   |
70 | 67, 69 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
   |
71 | 66, 70 | sylan9bb 706 |
. . . . . . . . . . . . . . . 16
 

    
   |
72 | 71 | adantrr 723 |
. . . . . . . . . . . . . . 15
 
           |
73 | 72 | ex 436 |
. . . . . . . . . . . . . 14
        
    |
74 | 73 | pm5.32rd 646 |
. . . . . . . . . . . . 13
      
  

      |
75 | | 3anass 989 |
. . . . . . . . . . . . 13
 


     |
76 | 74, 75 | syl6bbr 267 |
. . . . . . . . . . . 12
      
  

    |
77 | 34 | eleq2d 2514 |
. . . . . . . . . . . . 13
         
         |
78 | | elin 3617 |
. . . . . . . . . . . . 13
                   |
79 | 77, 78 | syl6bb 265 |
. . . . . . . . . . . 12
         
             |
80 | 65, 76, 79 | 3imtr4d 272 |
. . . . . . . . . . 11
      
              |
81 | 59, 80 | syl5bi 221 |
. . . . . . . . . 10
      

           |
82 | 81 | imp 431 |
. . . . . . . . 9
 
    
            |
83 | 82 | adantlr 721 |
. . . . . . . 8
   
 
    
            |
84 | 17 | adantlr 721 |
. . . . . . . 8
   
 
     |
85 | | simprl 764 |
. . . . . . . 8
 

    |
86 | | simprr 766 |
. . . . . . . 8
 

    |
87 | 2, 5, 14, 56, 58, 6, 83, 84, 28, 8, 85, 86 | tchcphlem1 22209 |
. . . . . . 7
 

                                        |
88 | 5, 8 | grpsubcl 16734 |
. . . . . . . . . 10
 
           |
89 | 88 | 3expb 1209 |
. . . . . . . . 9
  
            |
90 | 13, 89 | sylan 474 |
. . . . . . . 8
 

            |
91 | | oveq12 6299 |
. . . . . . . . . . 11
         
                               |
92 | 91 | anidms 651 |
. . . . . . . . . 10
         
                     |
93 | 92 | fveq2d 5869 |
. . . . . . . . 9
                                       |
94 | 93, 19, 24 | fvmpt3i 5953 |
. . . . . . . 8
        
                                            |
95 | 90, 94 | syl 17 |
. . . . . . 7
 

       
                                      |
96 | | oveq12 6299 |
. . . . . . . . . . . 12
 
       |
97 | 96 | anidms 651 |
. . . . . . . . . . 11
 
     |
98 | 97 | fveq2d 5869 |
. . . . . . . . . 10
          
    |
99 | 98, 19, 24 | fvmpt3i 5953 |
. . . . . . . . 9
      
              |
100 | 25, 99 | oveqan12d 6309 |
. . . . . . . 8
 
                   
           
           |
101 | 100 | adantl 468 |
. . . . . . 7
 

                    
           
           |
102 | 87, 95, 101 | 3brtr4d 4433 |
. . . . . 6
 

       
                                          |
103 | 7, 5, 8, 9, 13, 20, 55, 102 | tngngpd 21661 |
. . . . 5

NrmGrp |
104 | | phllmod 19197 |
. . . . . 6
   |
105 | 4, 104 | syl 17 |
. . . . 5
   |
106 | | cnnrg 21801 |
. . . . . . 7
ℂfld NrmRing |
107 | 33 | simp3d 1022 |
. . . . . . 7
     SubRing ℂfld  |
108 | | eqid 2451 |
. . . . . . . 8
ℂfld
↾s      ℂfld ↾s       |
109 | 108 | subrgnrg 21676 |
. . . . . . 7
 ℂfld NrmRing     SubRing ℂfld ℂfld ↾s
     NrmRing |
110 | 106, 107,
109 | sylancr 669 |
. . . . . 6
 ℂfld ↾s     
NrmRing |
111 | 57, 110 | eqeltrd 2529 |
. . . . 5

NrmRing |
112 | 103, 105,
111 | 3jca 1188 |
. . . 4
  NrmGrp
NrmRing  |
113 | 1 | adantr 467 |
. . . . . . 7
 
    
 
  |
114 | 57 | adantr 467 |
. . . . . . 7
 
    
 
ℂfld
↾s        |
115 | 82 | adantlr 721 |
. . . . . . 7
          
   
            |
116 | 17 | adantlr 721 |
. . . . . . 7
         

    |
117 | | eqid 2451 |
. . . . . . 7
         |
118 | | simprl 764 |
. . . . . . 7
 
    
        |
119 | | simprr 766 |
. . . . . . 7
 
    
    |
120 | 2, 5, 14, 113, 114, 6, 115, 116, 28, 117, 118, 119 | tchcphlem2 22210 |
. . . . . 6
 
    
                                
     |
121 | 13 | adantr 467 |
. . . . . . 7
 
    
 
  |
122 | 5, 14, 117, 28 | lmodvscl 18108 |
. . . . . . . . 9
     
           |
123 | 122 | 3expb 1209 |
. . . . . . . 8
                   |
124 | 11, 123 | sylan 474 |
. . . . . . 7
 
    
            |
125 | | eqid 2451 |
. . . . . . . 8
         |
126 | 2, 125, 5, 6 | tchnmval 22203 |
. . . . . . 7
                                                   |
127 | 121, 124,
126 | syl2anc 667 |
. . . . . 6
 
    
                                          |
128 | 114 | fveq2d 5869 |
. . . . . . . . 9
 
    
         ℂfld ↾s
        |
129 | 128 | fveq1d 5867 |
. . . . . . . 8
 
    
              ℂfld ↾s            |
130 | | subrgsubg 18014 |
. . . . . . . . . . 11
     SubRing ℂfld
    SubGrp ℂfld  |
131 | 107, 130 | syl 17 |
. . . . . . . . . 10
     SubGrp ℂfld  |
132 | 131 | adantr 467 |
. . . . . . . . 9
 
    
      SubGrp ℂfld  |
133 | | cnfldnm 21799 |
. . . . . . . . . 10
  ℂfld |
134 | | eqid 2451 |
. . . . . . . . . 10
   ℂfld ↾s          ℂfld
↾s        |
135 | 108, 133,
134 | subgnm2 21642 |
. . . . . . . . 9
      SubGrp ℂfld
         ℂfld ↾s                |
136 | 132, 118,
135 | syl2anc 667 |
. . . . . . . 8
 
    
      ℂfld ↾s
               |
137 | 129, 136 | eqtrd 2485 |
. . . . . . 7
 
    
                |
138 | 2, 125, 5, 6 | tchnmval 22203 |
. . . . . . . 8
 
            
    |
139 | 121, 119,
138 | syl2anc 667 |
. . . . . . 7
 
    
             
    |
140 | 137, 139 | oveq12d 6308 |
. . . . . 6
 
    
                                  |
141 | 120, 127,
140 | 3eqtr4d 2495 |
. . . . 5
 
    
                                      |
142 | 141 | ralrimivva 2809 |
. . . 4
       
                                    |
143 | 2, 5 | tchbas 22193 |
. . . . 5
     |
144 | 2, 117 | tchvsca 22198 |
. . . . 5
         |
145 | 2, 14 | tchsca 22197 |
. . . . 5
Scalar   |
146 | | eqid 2451 |
. . . . 5
         |
147 | 143, 125,
144, 145, 28, 146 | isnlm 21678 |
. . . 4
 NrmMod   NrmGrp
NrmRing 
     
                                     |
148 | 112, 142,
147 | sylanbrc 670 |
. . 3

NrmMod |
149 | 4, 148, 57 | 3jca 1188 |
. 2
  NrmMod
ℂfld ↾s         |
150 | | elin 3617 |
. . . . . 6
       
      
      |
151 | | elrege0 11738 |
. . . . . . 7
   
    |
152 | 151 | anbi2i 700 |
. . . . . 6
         
    
     |
153 | 150, 152 | bitri 253 |
. . . . 5
       
      
     |
154 | 153, 80 | syl5bi 221 |
. . . 4
      
               |
155 | 154 | ralrimiv 2800 |
. . 3
      
               |
156 | | sqrtf 13426 |
. . . . 5
     |
157 | | ffun 5731 |
. . . . 5
       |
158 | 156, 157 | ax-mp 5 |
. . . 4
 |
159 | | inss1 3652 |
. . . . . 6
              |
160 | 159, 36 | syl5ss 3443 |
. . . . 5
     
      |
161 | 156 | fdmi 5734 |
. . . . 5
 |
162 | 160, 161 | syl6sseqr 3479 |
. . . 4
     
   
  |
163 | | funimass4 5916 |
. . . 4
 
         
          
      
     
                |
164 | 158, 162,
163 | sylancr 669 |
. . 3
                                         |
165 | 155, 164 | mpbird 236 |
. 2
                    |
166 | | eqid 2451 |
. . . . 5
            
    |
167 | 42, 166 | fmptd 6046 |
. . . 4
     
         |
168 | 2, 5, 6 | tchval 22192 |
. . . . 5
 toNrmGrp

         |
169 | | cnex 9620 |
. . . . 5
 |
170 | 168, 5, 169 | tngnm 21659 |
. . . 4
      
       
              |
171 | 13, 167, 170 | syl2anc 667 |
. . 3
     
         |
172 | 171 | eqcomd 2457 |
. 2
               |
173 | 2, 6 | tchip 22199 |
. . 3
     |
174 | 143, 173,
125, 145, 28 | iscph 22148 |
. 2
   NrmMod ℂfld ↾s                
               
      |
175 | 149, 165,
172, 174 | syl3anbrc 1192 |
1
   |