Step | Hyp | Ref
| Expression |
1 | | inss2 3665 |
. . . . . . . 8
NrmRing   |
2 | 1 | sseli 3440 |
. . . . . . 7
 NrmRing 
  |
3 | 2 | 3ad2ant1 1035 |
. . . . . 6
  NrmRing  NrmMod chr  
  |
4 | | simp3 1016 |
. . . . . 6
  NrmRing  NrmMod chr  
chr    |
5 | | eqid 2462 |
. . . . . . 7
         |
6 | | eqid 2462 |
. . . . . . 7
/r  /r   |
7 | | eqid 2462 |
. . . . . . 7
 RHom   RHom   |
8 | 5, 6, 7 | qqhf 28839 |
. . . . . 6
  chr  
QQHom            |
9 | 3, 4, 8 | syl2anc 671 |
. . . . 5
  NrmRing  NrmMod chr  
QQHom            |
10 | | simpr 467 |
. . . . . . 7
   NrmRing  NrmMod chr  
   |
11 | | qsscn 11304 |
. . . . . . . . . . . . . 14
 |
12 | | simpr 467 |
. . . . . . . . . . . . . 14
    NrmRing

NrmMod chr   
   |
13 | 11, 12 | sseldi 3442 |
. . . . . . . . . . . . 13
    NrmRing

NrmMod chr   
   |
14 | | 0cn 9661 |
. . . . . . . . . . . . . . 15
 |
15 | | eqid 2462 |
. . . . . . . . . . . . . . . 16

  |
16 | 15 | cnmetdval 21840 |
. . . . . . . . . . . . . . 15
 
   
          |
17 | 14, 16 | mpan 681 |
. . . . . . . . . . . . . 14
              |
18 | | df-neg 9889 |
. . . . . . . . . . . . . . . 16
    |
19 | 18 | fveq2i 5891 |
. . . . . . . . . . . . . . 15
            |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
              |
21 | | absneg 13389 |
. . . . . . . . . . . . . 14
            |
22 | 17, 20, 21 | 3eqtr2d 2502 |
. . . . . . . . . . . . 13
            |
23 | 13, 22 | syl 17 |
. . . . . . . . . . . 12
    NrmRing

NrmMod chr   
            |
24 | | zssq 11300 |
. . . . . . . . . . . . . . 15
 |
25 | | 0z 10977 |
. . . . . . . . . . . . . . 15
 |
26 | 24, 25 | sselii 3441 |
. . . . . . . . . . . . . 14
 |
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
    NrmRing

NrmMod chr   
   |
28 | 27, 12 | ovresd 6464 |
. . . . . . . . . . . 12
    NrmRing

NrmMod chr   
    
            |
29 | | eqid 2462 |
. . . . . . . . . . . . . 14
         |
30 | | qqhcn.z |
. . . . . . . . . . . . . 14
 Mod   |
31 | 29, 30 | qqhnm 28843 |
. . . . . . . . . . . . 13
   NrmRing  NrmMod chr  
         QQHom            |
32 | 31 | adantlr 726 |
. . . . . . . . . . . 12
    NrmRing

NrmMod chr   
         QQHom            |
33 | 23, 28, 32 | 3eqtr4d 2506 |
. . . . . . . . . . 11
    NrmRing

NrmMod chr   
    
             QQHom        |
34 | 9 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    NrmRing

NrmMod chr   
 QQHom            |
35 | 34, 27 | ffvelrnd 6046 |
. . . . . . . . . . . . 13
    NrmRing

NrmMod chr   
  QQHom           |
36 | 34, 12 | ffvelrnd 6046 |
. . . . . . . . . . . . 13
    NrmRing

NrmMod chr   
  QQHom           |
37 | 35, 36 | ovresd 6464 |
. . . . . . . . . . . 12
    NrmRing

NrmMod chr   
   QQHom                        QQHom        QQHom            QQHom        |
38 | | inss1 3664 |
. . . . . . . . . . . . . . . . 17
NrmRing  NrmRing |
39 | 38 | sseli 3440 |
. . . . . . . . . . . . . . . 16
 NrmRing 
NrmRing |
40 | 39 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . 15
  NrmRing  NrmMod chr  
NrmRing |
41 | 40 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    NrmRing

NrmMod chr   
 NrmRing |
42 | | nrgngp 21714 |
. . . . . . . . . . . . . 14
 NrmRing NrmGrp |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
    NrmRing

NrmMod chr   
 NrmGrp |
44 | | eqid 2462 |
. . . . . . . . . . . . . 14
         |
45 | | eqid 2462 |
. . . . . . . . . . . . . 14
         |
46 | 29, 5, 44, 45 | ngpdsr 21667 |
. . . . . . . . . . . . 13
  NrmGrp
 QQHom        
 QQHom            QQHom            QQHom               QQHom            QQHom         |
47 | 43, 35, 36, 46 | syl3anc 1276 |
. . . . . . . . . . . 12
    NrmRing

NrmMod chr   
   QQHom            QQHom               QQHom            QQHom         |
48 | 3 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
    NrmRing

NrmMod chr   
   |
49 | 4 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
    NrmRing

NrmMod chr   
 chr    |
50 | 5, 6, 7 | qqh0 28837 |
. . . . . . . . . . . . . . . 16
  chr  
 QQHom           |
51 | 48, 49, 50 | syl2anc 671 |
. . . . . . . . . . . . . . 15
    NrmRing

NrmMod chr   
  QQHom           |
52 | 51 | oveq2d 6331 |
. . . . . . . . . . . . . 14
    NrmRing

NrmMod chr   
   QQHom            QQHom        QQHom                  |
53 | | ngpgrp 21662 |
. . . . . . . . . . . . . . . 16
 NrmGrp   |
54 | 43, 53 | syl 17 |
. . . . . . . . . . . . . . 15
    NrmRing

NrmMod chr   
   |
55 | | eqid 2462 |
. . . . . . . . . . . . . . . 16
         |
56 | 5, 55, 44 | grpsubid1 16788 |
. . . . . . . . . . . . . . 15
   QQHom         
  QQHom                 QQHom       |
57 | 54, 36, 56 | syl2anc 671 |
. . . . . . . . . . . . . 14
    NrmRing

NrmMod chr   
   QQHom                 QQHom       |
58 | 52, 57 | eqtrd 2496 |
. . . . . . . . . . . . 13
    NrmRing

NrmMod chr   
   QQHom            QQHom       QQHom       |
59 | 58 | fveq2d 5892 |
. . . . . . . . . . . 12
    NrmRing

NrmMod chr   
          QQHom            QQHom               QQHom        |
60 | 37, 47, 59 | 3eqtrd 2500 |
. . . . . . . . . . 11
    NrmRing

NrmMod chr   
   QQHom                        QQHom              QQHom        |
61 | 33, 60 | eqtr4d 2499 |
. . . . . . . . . 10
    NrmRing

NrmMod chr   
    
       QQHom                        QQHom        |
62 | 61 | breq1d 4426 |
. . . . . . . . 9
    NrmRing

NrmMod chr   
          
  QQHom                        QQHom         |
63 | 62 | biimpd 212 |
. . . . . . . 8
    NrmRing

NrmMod chr   
             QQHom                        QQHom         |
64 | 63 | ralrimiva 2814 |
. . . . . . 7
   NrmRing  NrmMod chr  
 
            QQHom                        QQHom         |
65 | | breq2 4420 |
. . . . . . . . . 10
          
   
        |
66 | 65 | imbi1d 323 |
. . . . . . . . 9
              QQHom                        QQHom           
       QQHom                        QQHom          |
67 | 66 | ralbidv 2839 |
. . . . . . . 8
  
            QQHom                        QQHom                    QQHom                        QQHom          |
68 | 67 | rspcev 3162 |
. . . . . . 7
  
            QQHom                        QQHom              
       QQHom                        QQHom         |
69 | 10, 64, 68 | syl2anc 671 |
. . . . . 6
   NrmRing  NrmMod chr  
 
     
       QQHom                        QQHom         |
70 | 69 | ralrimiva 2814 |
. . . . 5
  NrmRing  NrmMod chr  
               QQHom                        QQHom         |
71 | | qqhcn.q |
. . . . . . . 8
ℂfld ↾s   |
72 | | cnfldxms 21846 |
. . . . . . . . 9
ℂfld   |
73 | | qex 11305 |
. . . . . . . . 9
 |
74 | | ressxms 21589 |
. . . . . . . . 9
 ℂfld 

ℂfld
↾s     |
75 | 72, 73, 74 | mp2an 683 |
. . . . . . . 8
ℂfld
↾s    |
76 | 71, 75 | eqeltri 2536 |
. . . . . . 7
  |
77 | 71 | qrngbas 24506 |
. . . . . . . 8
     |
78 | | cnfldds 19029 |
. . . . . . . . . 10

  ℂfld |
79 | 71, 78 | ressds 15360 |
. . . . . . . . 9
        |
80 | 73, 79 | ax-mp 5 |
. . . . . . . 8

     |
81 | 77, 80 | xmsxmet2 21523 |
. . . . . . 7
   
          |
82 | 76, 81 | mp1i 13 |
. . . . . 6
  NrmRing  NrmMod chr  
  
         |
83 | | ngpxms 21664 |
. . . . . . . . 9
 NrmGrp    |
84 | 39, 42, 83 | 3syl 18 |
. . . . . . . 8
 NrmRing 
   |
85 | 84 | 3ad2ant1 1035 |
. . . . . . 7
  NrmRing  NrmMod chr  
   |
86 | 5, 45 | xmsxmet2 21523 |
. . . . . . 7
                             |
87 | 85, 86 | syl 17 |
. . . . . 6
  NrmRing  NrmMod chr  
                           |
88 | 26 | a1i 11 |
. . . . . 6
  NrmRing  NrmMod chr  
  |
89 | | qqhcn.j |
. . . . . . . . 9
     |
90 | 80 | reseq1i 5120 |
. . . . . . . . 9
              |
91 | 89, 77, 90 | xmstopn 21515 |
. . . . . . . 8
      
      |
92 | 76, 91 | ax-mp 5 |
. . . . . . 7
     
    |
93 | | eqid 2462 |
. . . . . . 7
                                         |
94 | 92, 93 | metcnp 21605 |
. . . . . 6
   
                                   QQHom                             QQHom                 
       QQHom                        QQHom           |
95 | 82, 87, 88, 94 | syl3anc 1276 |
. . . . 5
  NrmRing  NrmMod chr  
 QQHom                             QQHom          
      
       QQHom                        QQHom           |
96 | 9, 70, 95 | mpbir2and 938 |
. . . 4
  NrmRing  NrmMod chr  
QQHom                              |
97 | | qqhcn.k |
. . . . . . . 8
     |
98 | | eqid 2462 |
. . . . . . . 8
                                 |
99 | 97, 5, 98 | xmstopn 21515 |
. . . . . . 7
                        |
100 | 85, 99 | syl 17 |
. . . . . 6
  NrmRing  NrmMod chr  
                      |
101 | 100 | oveq2d 6331 |
. . . . 5
  NrmRing  NrmMod chr  
                          |
102 | 101 | fveq1d 5890 |
. . . 4
  NrmRing  NrmMod chr  
                                  |
103 | 96, 102 | eleqtrrd 2543 |
. . 3
  NrmRing  NrmMod chr  
QQHom          |
104 | | cnfldtgp 21950 |
. . . . . 6
ℂfld  |
105 | | qsubdrg 19069 |
. . . . . . . 8
 SubRing ℂfld
ℂfld ↾s
   |
106 | 105 | simpli 464 |
. . . . . . 7
SubRing ℂfld |
107 | | subrgsubg 18063 |
. . . . . . 7
 SubRing ℂfld
SubGrp ℂfld  |
108 | 106, 107 | ax-mp 5 |
. . . . . 6
SubGrp ℂfld |
109 | 71 | subgtgp 21169 |
. . . . . 6
 ℂfld SubGrp ℂfld   |
110 | 104, 108,
109 | mp2an 683 |
. . . . 5
 |
111 | | tgptmd 21143 |
. . . . 5
 TopMnd |
112 | 110, 111 | mp1i 13 |
. . . 4
  NrmRing  NrmMod chr  
TopMnd |
113 | | nrgtrg 21741 |
. . . . 5
 NrmRing   |
114 | | trgtmd2 21232 |
. . . . 5
 TopMnd |
115 | 40, 113, 114 | 3syl 18 |
. . . 4
  NrmRing  NrmMod chr  
TopMnd |
116 | 5, 6, 7, 71 | qqhghm 28841 |
. . . . 5
  chr  
QQHom      |
117 | 3, 4, 116 | syl2anc 671 |
. . . 4
  NrmRing  NrmMod chr  
QQHom      |
118 | 77, 89, 97 | ghmcnp 21178 |
. . . 4
  TopMnd
TopMnd QQHom    
 QQHom         QQHom        |
119 | 112, 115,
117, 118 | syl3anc 1276 |
. . 3
  NrmRing  NrmMod chr  
 QQHom         QQHom        |
120 | 103, 119 | mpbid 215 |
. 2
  NrmRing  NrmMod chr  
 QQHom       |
121 | 120 | simprd 469 |
1
  NrmRing  NrmMod chr  
QQHom      |