Step | Hyp | Ref
| Expression |
1 | | inss2 3522 |
. . . . . . . 8
NrmRing   |
2 | 1 | sseli 3304 |
. . . . . . 7
 NrmRing 
  |
3 | 2 | 3ad2ant1 978 |
. . . . . 6
  NrmRing  NrmMod chr  
  |
4 | | simp3 959 |
. . . . . 6
  NrmRing  NrmMod chr  
chr    |
5 | | eqid 2404 |
. . . . . . 7
         |
6 | | eqid 2404 |
. . . . . . 7
/r  /r   |
7 | | eqid 2404 |
. . . . . . 7
 RHom   RHom   |
8 | 5, 6, 7 | qqhf 24323 |
. . . . . 6
  chr  
QQHom            |
9 | 3, 4, 8 | syl2anc 643 |
. . . . 5
  NrmRing  NrmMod chr  
QQHom            |
10 | | simpr 448 |
. . . . . . 7
   NrmRing  NrmMod chr  
   |
11 | | qsscn 10541 |
. . . . . . . . . . . . . 14
 |
12 | | simpr 448 |
. . . . . . . . . . . . . 14
    NrmRing

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

NrmMod chr   
   |
14 | | 0cn 9040 |
. . . . . . . . . . . . . . 15
 |
15 | | eqid 2404 |
. . . . . . . . . . . . . . . 16

  |
16 | 15 | cnmetdval 18758 |
. . . . . . . . . . . . . . 15
 
   
          |
17 | 14, 16 | mpan 652 |
. . . . . . . . . . . . . 14
              |
18 | | df-neg 9250 |
. . . . . . . . . . . . . . . 16
    |
19 | 18 | fveq2i 5690 |
. . . . . . . . . . . . . . 15
            |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
              |
21 | | absneg 12037 |
. . . . . . . . . . . . . 14
            |
22 | 17, 20, 21 | 3eqtr2d 2442 |
. . . . . . . . . . . . 13
            |
23 | 13, 22 | syl 16 |
. . . . . . . . . . . 12
    NrmRing

NrmMod chr   
            |
24 | | zssq 10537 |
. . . . . . . . . . . . . . 15
 |
25 | | 0z 10249 |
. . . . . . . . . . . . . . 15
 |
26 | 24, 25 | sselii 3305 |
. . . . . . . . . . . . . 14
 |
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
    NrmRing

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

NrmMod chr   
    
            |
29 | | eqid 2404 |
. . . . . . . . . . . . . 14
         |
30 | | qqhcn.z |
. . . . . . . . . . . . . 14
 Mod   |
31 | 29, 30 | qqhnm 24327 |
. . . . . . . . . . . . 13
   NrmRing  NrmMod chr  
         QQHom            |
32 | 31 | adantlr 696 |
. . . . . . . . . . . 12
    NrmRing

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

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

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

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

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

NrmMod chr   
   QQHom                        QQHom        QQHom            QQHom        |
38 | | inss1 3521 |
. . . . . . . . . . . . . . . . 17
NrmRing  NrmRing |
39 | 38 | sseli 3304 |
. . . . . . . . . . . . . . . 16
 NrmRing 
NrmRing |
40 | 39 | 3ad2ant1 978 |
. . . . . . . . . . . . . . 15
  NrmRing  NrmMod chr  
NrmRing |
41 | 40 | ad2antrr 707 |
. . . . . . . . . . . . . 14
    NrmRing

NrmMod chr   
 NrmRing |
42 | | nrgngp 18651 |
. . . . . . . . . . . . . 14
 NrmRing NrmGrp |
43 | 41, 42 | syl 16 |
. . . . . . . . . . . . 13
    NrmRing

NrmMod chr   
 NrmGrp |
44 | | eqid 2404 |
. . . . . . . . . . . . . 14
         |
45 | | eqid 2404 |
. . . . . . . . . . . . . 14
         |
46 | 29, 5, 44, 45 | ngpdsr 18604 |
. . . . . . . . . . . . 13
  NrmGrp
 QQHom        
 QQHom            QQHom            QQHom               QQHom            QQHom         |
47 | 43, 35, 36, 46 | syl3anc 1184 |
. . . . . . . . . . . 12
    NrmRing

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

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

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

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

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

NrmMod chr   
   |
55 | | eqid 2404 |
. . . . . . . . . . . . . . . 16
         |
56 | 5, 55, 44 | grpsubid1 14829 |
. . . . . . . . . . . . . . 15
   QQHom         
  QQHom                 QQHom       |
57 | 54, 36, 56 | syl2anc 643 |
. . . . . . . . . . . . . 14
    NrmRing

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

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

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

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

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

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

NrmMod chr   
             QQHom                        QQHom         |
64 | 63 | ralrimiva 2749 |
. . . . . . 7
   NrmRing  NrmMod chr  
 
            QQHom                        QQHom         |
65 | | breq2 4176 |
. . . . . . . . . 10
          
   
        |
66 | 65 | imbi1d 309 |
. . . . . . . . 9
              QQHom                        QQHom           
       QQHom                        QQHom          |
67 | 66 | ralbidv 2686 |
. . . . . . . 8
  
            QQHom                        QQHom                    QQHom                        QQHom          |
68 | 67 | rspcev 3012 |
. . . . . . 7
  
            QQHom                        QQHom              
       QQHom                        QQHom         |
69 | 10, 64, 68 | syl2anc 643 |
. . . . . 6
   NrmRing  NrmMod chr  
 
     
       QQHom                        QQHom         |
70 | 69 | ralrimiva 2749 |
. . . . 5
  NrmRing  NrmMod chr  
               QQHom                        QQHom         |
71 | | qqhcn.q |
. . . . . . . 8
ℂfld ↾s   |
72 | | cnfldxms 18764 |
. . . . . . . . 9
ℂfld   |
73 | | qex 10542 |
. . . . . . . . 9
 |
74 | | ressxms 18508 |
. . . . . . . . 9
 ℂfld 

ℂfld
↾s     |
75 | 72, 73, 74 | mp2an 654 |
. . . . . . . 8
ℂfld
↾s    |
76 | 71, 75 | eqeltri 2474 |
. . . . . . 7
  |
77 | 71 | qrngbas 21266 |
. . . . . . . 8
     |
78 | | cnfldds 16668 |
. . . . . . . . . 10

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

     |
81 | 77, 80 | xmsxmet2 18442 |
. . . . . . 7
   
          |
82 | 76, 81 | mp1i 12 |
. . . . . 6
  NrmRing  NrmMod chr  
  
         |
83 | | ngpxms 18601 |
. . . . . . . . 9
 NrmGrp    |
84 | 39, 42, 83 | 3syl 19 |
. . . . . . . 8
 NrmRing 
   |
85 | 84 | 3ad2ant1 978 |
. . . . . . 7
  NrmRing  NrmMod chr  
   |
86 | 5, 45 | xmsxmet2 18442 |
. . . . . . 7
                             |
87 | 85, 86 | syl 16 |
. . . . . 6
  NrmRing  NrmMod chr  
                           |
88 | 26 | a1i 11 |
. . . . . 6
  NrmRing  NrmMod chr  
  |
89 | | qqhcn.j |
. . . . . . . . 9
     |
90 | 80 | reseq1i 5101 |
. . . . . . . . 9
              |
91 | 89, 77, 90 | xmstopn 18434 |
. . . . . . . 8
      
      |
92 | 76, 91 | ax-mp 8 |
. . . . . . 7
     
    |
93 | | eqid 2404 |
. . . . . . 7
                                         |
94 | 92, 93 | metcnp 18524 |
. . . . . 6
   
                                   QQHom                             QQHom                 
       QQHom                        QQHom           |
95 | 82, 87, 88, 94 | syl3anc 1184 |
. . . . 5
  NrmRing  NrmMod chr  
 QQHom                             QQHom          
      
       QQHom                        QQHom           |
96 | 9, 70, 95 | mpbir2and 889 |
. . . 4
  NrmRing  NrmMod chr  
QQHom                              |
97 | | qqhcn.k |
. . . . . . . 8
     |
98 | | eqid 2404 |
. . . . . . . 8
                                 |
99 | 97, 5, 98 | xmstopn 18434 |
. . . . . . 7
                        |
100 | 85, 99 | syl 16 |
. . . . . 6
  NrmRing  NrmMod chr  
                      |
101 | 100 | oveq2d 6056 |
. . . . 5
  NrmRing  NrmMod chr  
                          |
102 | 101 | fveq1d 5689 |
. . . 4
  NrmRing  NrmMod chr  
                                  |
103 | 96, 102 | eleqtrrd 2481 |
. . 3
  NrmRing  NrmMod chr  
QQHom          |
104 | | cnfldtgp 18852 |
. . . . . 6
ℂfld  |
105 | | qsubdrg 16706 |
. . . . . . . 8
 SubRing ℂfld
ℂfld ↾s
   |
106 | 105 | simpli 445 |
. . . . . . 7
SubRing ℂfld |
107 | | subrgsubg 15829 |
. . . . . . 7
 SubRing ℂfld
SubGrp ℂfld  |
108 | 106, 107 | ax-mp 8 |
. . . . . 6
SubGrp ℂfld |
109 | 71 | subgtgp 18088 |
. . . . . 6
 ℂfld SubGrp ℂfld   |
110 | 104, 108,
109 | mp2an 654 |
. . . . 5
 |
111 | | tgptmd 18062 |
. . . . 5
 TopMnd |
112 | 110, 111 | mp1i 12 |
. . . 4
  NrmRing  NrmMod chr  
TopMnd |
113 | | nrgtrg 18678 |
. . . . 5
 NrmRing   |
114 | | trgtmd2 18151 |
. . . . 5
 TopMnd |
115 | 40, 113, 114 | 3syl 19 |
. . . 4
  NrmRing  NrmMod chr  
TopMnd |
116 | 5, 6, 7, 71 | qqhghm 24325 |
. . . . 5
  chr  
QQHom      |
117 | 3, 4, 116 | syl2anc 643 |
. . . 4
  NrmRing  NrmMod chr  
QQHom      |
118 | 77, 89, 97 | ghmcnp 18097 |
. . . 4
  TopMnd
TopMnd QQHom    
 QQHom         QQHom        |
119 | 112, 115,
117, 118 | syl3anc 1184 |
. . 3
  NrmRing  NrmMod chr  
 QQHom         QQHom        |
120 | 103, 119 | mpbid 202 |
. 2
  NrmRing  NrmMod chr  
 QQHom       |
121 | 120 | simprd 450 |
1
  NrmRing  NrmMod chr  
QQHom      |