Step | Hyp | Ref
| Expression |
1 | | nrgring 21715 |
. . . 4
 NrmRing   |
2 | | nrginvrcn.u |
. . . . 5
Unit   |
3 | | eqid 2462 |
. . . . 5
 mulGrp 
↾s   mulGrp  ↾s   |
4 | 2, 3 | unitgrp 17944 |
. . . 4

 mulGrp 
↾s    |
5 | 2, 3 | unitgrpbas 17943 |
. . . . 5
    mulGrp  ↾s    |
6 | | nrginvrcn.i |
. . . . . 6
     |
7 | 2, 3, 6 | invrfval 17950 |
. . . . 5
     mulGrp  ↾s    |
8 | 5, 7 | grpinvf 16759 |
. . . 4
  mulGrp  ↾s        |
9 | 1, 4, 8 | 3syl 18 |
. . 3
 NrmRing       |
10 | | 1rp 11335 |
. . . . . . . 8
 |
11 | 10 | ne0ii 3750 |
. . . . . . 7
 |
12 | 1 | ad2antrr 737 |
. . . . . . . . . . . . . 14
   NrmRing 
  
  |
13 | | nrginvrcn.x |
. . . . . . . . . . . . . . . 16
     |
14 | 13, 2 | unitss 17937 |
. . . . . . . . . . . . . . 15
 |
15 | | simplrl 775 |
. . . . . . . . . . . . . . 15
   NrmRing 
  
  |
16 | 14, 15 | sseldi 3442 |
. . . . . . . . . . . . . 14
   NrmRing 
  
  |
17 | | simpr 467 |
. . . . . . . . . . . . . . 15
   NrmRing 
  
  |
18 | 14, 17 | sseldi 3442 |
. . . . . . . . . . . . . 14
   NrmRing 
  
  |
19 | | eqid 2462 |
. . . . . . . . . . . . . . 15
         |
20 | | eqid 2462 |
. . . . . . . . . . . . . . 15
         |
21 | 13, 19, 20 | ring1eq0 17869 |
. . . . . . . . . . . . . 14
 
         
   |
22 | 12, 16, 18, 21 | syl3anc 1276 |
. . . . . . . . . . . . 13
   NrmRing 
  
        
   |
23 | | eqid 2462 |
. . . . . . . . . . . . . . . 16
         |
24 | | nrgngp 21714 |
. . . . . . . . . . . . . . . . . . 19
 NrmRing NrmGrp |
25 | | ngpms 21663 |
. . . . . . . . . . . . . . . . . . 19
 NrmGrp   |
26 | | msxms 21518 |
. . . . . . . . . . . . . . . . . . 19

   |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
 NrmRing    |
28 | 27 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
   NrmRing 
  
   |
29 | 9 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
  NrmRing

        |
30 | 29 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . 18
   NrmRing 
  
      |
31 | 14, 30 | sseldi 3442 |
. . . . . . . . . . . . . . . . 17
   NrmRing 
  
      |
32 | | eqid 2462 |
. . . . . . . . . . . . . . . . . 18
         |
33 | 13, 32 | xmseq0 21528 |
. . . . . . . . . . . . . . . . 17
                                        |
34 | 28, 31, 31, 33 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
   NrmRing 
  
                            |
35 | 23, 34 | mpbiri 241 |
. . . . . . . . . . . . . . 15
   NrmRing 
  
                  |
36 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
   NrmRing 
  
  |
37 | 36 | rpgt0d 11373 |
. . . . . . . . . . . . . . 15
   NrmRing 
  
  |
38 | 35, 37 | eqbrtrd 4437 |
. . . . . . . . . . . . . 14
   NrmRing 
  
                  |
39 | | fveq2 5888 |
. . . . . . . . . . . . . . . 16
           |
40 | 39 | oveq1d 6330 |
. . . . . . . . . . . . . . 15
                                   |
41 | 40 | breq1d 4426 |
. . . . . . . . . . . . . 14
                 
                   |
42 | 38, 41 | syl5ibrcom 230 |
. . . . . . . . . . . . 13
   NrmRing 
  

                   |
43 | 22, 42 | syld 45 |
. . . . . . . . . . . 12
   NrmRing 
  
        
                   |
44 | 43 | imp 435 |
. . . . . . . . . . 11
    NrmRing 
 
                            |
45 | 44 | an32s 818 |
. . . . . . . . . 10
    NrmRing 
 
                            |
46 | 45 | a1d 26 |
. . . . . . . . 9
    NrmRing 
 
                                      |
47 | 46 | ralrimiva 2814 |
. . . . . . . 8
   NrmRing 
          

        
                   |
48 | 47 | ralrimivw 2815 |
. . . . . . 7
   NrmRing 
          
          
                   |
49 | | r19.2z 3870 |
. . . . . . 7
 


        
                            
                   |
50 | 11, 48, 49 | sylancr 674 |
. . . . . 6
   NrmRing 
          
          
                   |
51 | | eqid 2462 |
. . . . . . 7
         |
52 | | simpll 765 |
. . . . . . 7
   NrmRing 
           NrmRing |
53 | 1 | ad2antrr 737 |
. . . . . . . 8
   NrmRing 
             |
54 | | simpr 467 |
. . . . . . . 8
   NrmRing 
                     |
55 | 19, 20 | isnzr 18532 |
. . . . . . . 8
 NzRing             |
56 | 53, 54, 55 | sylanbrc 675 |
. . . . . . 7
   NrmRing 
           NzRing |
57 | | simplrl 775 |
. . . . . . 7
   NrmRing 
             |
58 | | simplrr 776 |
. . . . . . 7
   NrmRing 
             |
59 | | eqid 2462 |
. . . . . . 7
                                       
                                   |
60 | 13, 2, 6, 51, 32, 52, 56, 57, 58, 59 | nrginvrcnlem 21742 |
. . . . . 6
   NrmRing 
                                         |
61 | 50, 60 | pm2.61dane 2723 |
. . . . 5
  NrmRing

                                |
62 | 15, 17 | ovresd 6464 |
. . . . . . . . 9
   NrmRing 
  
                      |
63 | 62 | breq1d 4426 |
. . . . . . . 8
   NrmRing 
  
                        |
64 | | simpl 463 |
. . . . . . . . . . . 12
 

  |
65 | | ffvelrn 6043 |
. . . . . . . . . . . 12
     
       |
66 | 9, 64, 65 | syl2an 484 |
. . . . . . . . . . 11
  NrmRing

        |
67 | 66 | adantr 471 |
. . . . . . . . . 10
   NrmRing 
  
      |
68 | 67, 30 | ovresd 6464 |
. . . . . . . . 9
   NrmRing 
  
                                      |
69 | 68 | breq1d 4426 |
. . . . . . . 8
   NrmRing 
  
                                        |
70 | 63, 69 | imbi12d 326 |
. . . . . . 7
   NrmRing 
  
                                           
                    |
71 | 70 | ralbidva 2836 |
. . . . . 6
  NrmRing

   
                                 

        
                    |
72 | 71 | rexbidv 2913 |
. . . . 5
  NrmRing

                                      
          
                    |
73 | 61, 72 | mpbird 240 |
. . . 4
  NrmRing

                                        |
74 | 73 | ralrimivva 2821 |
. . 3
 NrmRing  
                                      |
75 | | xpss12 4959 |
. . . . . . 7
 
  
    |
76 | 14, 14, 75 | mp2an 683 |
. . . . . 6
  
  |
77 | | resabs1 5152 |
. . . . . 6
              
            |
78 | 76, 77 | ax-mp 5 |
. . . . 5
         
           |
79 | | eqid 2462 |
. . . . . . . 8
                 |
80 | 13, 79 | xmsxmet 21520 |
. . . . . . 7
                 |
81 | 24, 25, 26, 80 | 4syl 19 |
. . . . . 6
 NrmRing                |
82 | | xmetres2 21425 |
. . . . . 6
                         
         |
83 | 81, 14, 82 | sylancl 673 |
. . . . 5
 NrmRing                    |
84 | 78, 83 | syl5eqelr 2545 |
. . . 4
 NrmRing                |
85 | | eqid 2462 |
. . . . 5
                         |
86 | 85, 85 | metcn 21607 |
. . . 4
                                                             

                                        |
87 | 84, 84, 86 | syl2anc 671 |
. . 3
 NrmRing                       
                                                   |
88 | 9, 74, 87 | mpbir2and 938 |
. 2
 NrmRing          
           
      |
89 | | nrginvrcn.j |
. . . . . . 7
     |
90 | 89, 13, 79 | mstopn 21516 |
. . . . . 6

        
     |
91 | 24, 25, 90 | 3syl 18 |
. . . . 5
 NrmRing               |
92 | 91 | oveq1d 6330 |
. . . 4
 NrmRing  ↾t               ↾t    |
93 | 78 | eqcomi 2471 |
. . . . . 6
                 
   |
94 | | eqid 2462 |
. . . . . 6
                         |
95 | 93, 94, 85 | metrest 21588 |
. . . . 5
                         
   ↾t                |
96 | 81, 14, 95 | sylancl 673 |
. . . 4
 NrmRing              ↾t                |
97 | 92, 96 | eqtrd 2496 |
. . 3
 NrmRing  ↾t                |
98 | 97, 97 | oveq12d 6333 |
. 2
 NrmRing   ↾t   ↾t            
           
      |
99 | 88, 98 | eleqtrrd 2543 |
1
 NrmRing  
↾t   ↾t     |