Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. . 3
DChr   |
2 | | dchrval.z |
. . 3
ℤ/nℤ   |
3 | | dchrval.b |
. . 3
     |
4 | | dchrval.u |
. . 3
Unit   |
5 | | dchrval.n |
. . 3
   |
6 | | dchrbas.b |
. . 3
     |
7 | 1, 2, 3, 4, 5, 6 | dchrelbas2 24158 |
. 2
    mulGrp  MndHom mulGrp ℂfld

    
     |
8 | | fveq2 5863 |
. . . . . . . 8
           |
9 | 8 | neeq1d 2682 |
. . . . . . 7
             |
10 | | eleq1 2516 |
. . . . . . 7
 
   |
11 | 9, 10 | imbi12d 322 |
. . . . . 6
                 |
12 | 11 | cbvralv 3018 |
. . . . 5
 
      
        |
13 | 5 | nnnn0d 10922 |
. . . . . . . . . . 11
   |
14 | 2 | zncrng 19108 |
. . . . . . . . . . 11

  |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
   |
16 | | crngring 17784 |
. . . . . . . . . 10

  |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
   |
18 | | eqid 2450 |
. . . . . . . . . 10
mulGrp  mulGrp   |
19 | 18 | ringmgp 17779 |
. . . . . . . . 9

mulGrp    |
20 | 17, 19 | syl 17 |
. . . . . . . 8
 mulGrp    |
21 | | cnring 18983 |
. . . . . . . . 9
ℂfld  |
22 | | eqid 2450 |
. . . . . . . . . 10
mulGrp ℂfld mulGrp ℂfld |
23 | 22 | ringmgp 17779 |
. . . . . . . . 9
ℂfld mulGrp ℂfld
  |
24 | 21, 23 | ax-mp 5 |
. . . . . . . 8
mulGrp ℂfld  |
25 | 18, 3 | mgpbas 17722 |
. . . . . . . . . 10
   mulGrp    |
26 | | cnfldbas 18967 |
. . . . . . . . . . 11
  ℂfld |
27 | 22, 26 | mgpbas 17722 |
. . . . . . . . . 10
   mulGrp ℂfld  |
28 | | eqid 2450 |
. . . . . . . . . . 11
         |
29 | 18, 28 | mgpplusg 17720 |
. . . . . . . . . 10
      mulGrp    |
30 | | cnfldmul 18969 |
. . . . . . . . . . 11
  ℂfld |
31 | 22, 30 | mgpplusg 17720 |
. . . . . . . . . 10
  mulGrp ℂfld  |
32 | | eqid 2450 |
. . . . . . . . . . 11
         |
33 | 18, 32 | ringidval 17730 |
. . . . . . . . . 10
       mulGrp    |
34 | | cnfld1 18986 |
. . . . . . . . . . 11
  ℂfld |
35 | 22, 34 | ringidval 17730 |
. . . . . . . . . 10
   mulGrp ℂfld  |
36 | 25, 27, 29, 31, 33, 35 | ismhm 16577 |
. . . . . . . . 9
  mulGrp 
MndHom mulGrp ℂfld
  mulGrp  mulGrp ℂfld        
                                  |
37 | 36 | baib 913 |
. . . . . . . 8
  mulGrp  mulGrp ℂfld  
 mulGrp  MndHom mulGrp ℂfld      

                                  |
38 | 20, 24, 37 | sylancl 667 |
. . . . . . 7
   mulGrp  MndHom mulGrp ℂfld
     

                                  |
39 | 38 | adantr 467 |
. . . . . 6
 

    
    mulGrp  MndHom mulGrp ℂfld
     

                                  |
40 | | biimt 337 |
. . . . . . . . . . . . . . 15
 
                                                     |
41 | 40 | adantl 468 |
. . . . . . . . . . . . . 14
                  
 

                                                      |
42 | 17 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . . . . 21
                 
 
  |
43 | | simprl 763 |
. . . . . . . . . . . . . . . . . . . . 21
                 
 
  |
44 | | simprr 765 |
. . . . . . . . . . . . . . . . . . . . 21
                 
 
  |
45 | 3, 28 | ringcl 17787 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
46 | 42, 43, 44, 45 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . 20
                 
 
          |
47 | | simpllr 768 |
. . . . . . . . . . . . . . . . . . . 20
                 
 

    
   |
48 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           |
49 | 48 | neeq1d 2682 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
50 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . 22
         
           |
51 | 49, 50 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . 21
                                         |
52 | 51 | rspcv 3145 |
. . . . . . . . . . . . . . . . . . . 20
          
                  
            |
53 | 46, 47, 52 | sylc 62 |
. . . . . . . . . . . . . . . . . . 19
                 
 
                        |
54 | 15 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . . . 20
                 
 
  |
55 | 4, 28, 3 | unitmulclb 17886 |
. . . . . . . . . . . . . . . . . . . 20
 
         

    |
56 | 54, 43, 44, 55 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . 19
                 
 
        

    |
57 | 53, 56 | sylibd 218 |
. . . . . . . . . . . . . . . . . 18
                 
 
             
    |
58 | 57 | necon1bd 2641 |
. . . . . . . . . . . . . . . . 17
                 
 
 

               |
59 | 58 | imp 431 |
. . . . . . . . . . . . . . . 16
                  
 

 
              |
60 | 11 | rspcv 3145 |
. . . . . . . . . . . . . . . . . . . . 21
  
          
    |
61 | 43, 47, 60 | sylc 62 |
. . . . . . . . . . . . . . . . . . . 20
                 
 
    
   |
62 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
63 | 62 | neeq1d 2682 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
64 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
65 | 63, 64 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
66 | 65 | rspcv 3145 |
. . . . . . . . . . . . . . . . . . . . 21
  
          
    |
67 | 44, 47, 66 | sylc 62 |
. . . . . . . . . . . . . . . . . . . 20
                 
 
    
   |
68 | 61, 67 | anim12d 566 |
. . . . . . . . . . . . . . . . . . 19
                 
 
                |
69 | 68 | con3dimp 443 |
. . . . . . . . . . . . . . . . . 18
                  
 

 
            |
70 | | neanior 2715 |
. . . . . . . . . . . . . . . . . . 19
                       |
71 | 70 | con2bii 334 |
. . . . . . . . . . . . . . . . . 18
                       |
72 | 69, 71 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
                  
 

 
            |
73 | | simplr 761 |
. . . . . . . . . . . . . . . . . . . 20
                 
 
      |
74 | 73, 43 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . 19
                 
 
      |
75 | 73, 44 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . 19
                 
 
      |
76 | 74, 75 | mul0ord 10259 |
. . . . . . . . . . . . . . . . . 18
                 
 
          
             |
77 | 76 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                  
 

 
          
             |
78 | 72, 77 | mpbird 236 |
. . . . . . . . . . . . . . . 16
                  
 

 
            |
79 | 59, 78 | eqtr4d 2487 |
. . . . . . . . . . . . . . 15
                  
 

 
                        |
80 | 79 | a1d 26 |
. . . . . . . . . . . . . . 15
                  
 

 
 
                          |
81 | 79, 80 | 2thd 244 |
. . . . . . . . . . . . . 14
                  
 

 
                      
 
                           |
82 | 41, 81 | pm2.61dan 799 |
. . . . . . . . . . . . 13
                 
 
                      
 
                           |
83 | 82 | pm5.74da 692 |
. . . . . . . . . . . 12
   
                                      
 
                               |
84 | 3, 4 | unitcl 17880 |
. . . . . . . . . . . . . . . 16
   |
85 | 3, 4 | unitcl 17880 |
. . . . . . . . . . . . . . . 16
   |
86 | 84, 85 | anim12i 569 |
. . . . . . . . . . . . . . 15
 
 
   |
87 | 86 | pm4.71ri 638 |
. . . . . . . . . . . . . 14
 
  


    |
88 | 87 | imbi1i 327 |
. . . . . . . . . . . . 13
  

                         
 
                           |
89 | | impexp 448 |
. . . . . . . . . . . . 13
     
 
                           

                          |
90 | 88, 89 | bitri 253 |
. . . . . . . . . . . 12
  

                           

                          |
91 | 83, 90 | syl6bbr 267 |
. . . . . . . . . . 11
   
                                      
 
                           |
92 | 91 | 2albidv 1768 |
. . . . . . . . . 10
   
                  

                                                        |
93 | | r2al 2765 |
. . . . . . . . . 10
 

                     
                                |
94 | | r2al 2765 |
. . . . . . . . . 10
 

                     
                                |
95 | 92, 93, 94 | 3bitr4g 292 |
. . . . . . . . 9
   
             

                     


                         |
96 | 95 | adantrr 722 |
. . . . . . . 8
   
                       

                      

                         |
97 | 96 | pm5.32da 646 |
. . . . . . 7
 

    
                   
                      
                
                          |
98 | | 3anan32 996 |
. . . . . . 7
       
                              
                
                         |
99 | | an31 808 |
. . . . . . 7
                                        
                
                         |
100 | 97, 98, 99 | 3bitr4g 292 |
. . . . . 6
 

    
        

                                 

                                       |
101 | 39, 100 | bitrd 257 |
. . . . 5
 

    
    mulGrp  MndHom mulGrp ℂfld
  

                                       |
102 | 12, 101 | sylan2br 479 |
. . . 4
 

    
    mulGrp  MndHom mulGrp ℂfld
  

                                       |
103 | 102 | pm5.32da 646 |
. . 3
   
    
  mulGrp  MndHom mulGrp ℂfld 
 
    
   

                                        |
104 | | ancom 452 |
. . 3
   mulGrp  MndHom mulGrp ℂfld

    
 
 
    

 mulGrp  MndHom mulGrp ℂfld    |
105 | | df-3an 986 |
. . . . 5
   
                              
    
 
  

                               
    
    |
106 | 105 | anbi2i 699 |
. . . 4
        
                              
    
          

                               
    
     |
107 | | an13 807 |
. . . 4
        

                                    
         
                                            |
108 | 106, 107 | bitri 253 |
. . 3
        
                              
    
         
                                            |
109 | 103, 104,
108 | 3bitr4g 292 |
. 2
    mulGrp  MndHom mulGrp ℂfld 
    
        

                              
    
      |
110 | 7, 109 | bitrd 257 |
1
         
                              
    
      |