Proof of Theorem issubdrg
Step | Hyp | Ref
| Expression |
1 | | simpllr 777 |
. . . . . 6
    SubRing  

  
SubRing    |
2 | | issubdrg.s |
. . . . . . 7

↾s   |
3 | 2 | subrgring 18089 |
. . . . . 6
 SubRing 
  |
4 | 1, 3 | syl 17 |
. . . . 5
    SubRing  

  
  |
5 | | simpr 468 |
. . . . . . . . 9
    SubRing  

  

   |
6 | | eldifsn 4088 |
. . . . . . . . 9
  

  |
7 | 5, 6 | sylib 201 |
. . . . . . . 8
    SubRing  

  

  |
8 | 7 | simpld 466 |
. . . . . . 7
    SubRing  

  
  |
9 | 2 | subrgbas 18095 |
. . . . . . . 8
 SubRing 
      |
10 | 1, 9 | syl 17 |
. . . . . . 7
    SubRing  

  
      |
11 | 8, 10 | eleqtrd 2551 |
. . . . . 6
    SubRing  

  
      |
12 | 7 | simprd 470 |
. . . . . . 7
    SubRing  

  
 |
13 | | issubdrg.z |
. . . . . . . . 9
     |
14 | 2, 13 | subrg0 18093 |
. . . . . . . 8
 SubRing 
      |
15 | 1, 14 | syl 17 |
. . . . . . 7
    SubRing  

  
      |
16 | 12, 15 | neeqtrd 2712 |
. . . . . 6
    SubRing  

  
      |
17 | | eqid 2471 |
. . . . . . . 8
         |
18 | | eqid 2471 |
. . . . . . . 8
Unit  Unit   |
19 | | eqid 2471 |
. . . . . . . 8
         |
20 | 17, 18, 19 | drngunit 18058 |
. . . . . . 7
  Unit               |
21 | 20 | ad2antlr 741 |
. . . . . 6
    SubRing  

  
 Unit               |
22 | 11, 16, 21 | mpbir2and 936 |
. . . . 5
    SubRing  

  
Unit    |
23 | | eqid 2471 |
. . . . . 6
         |
24 | 18, 23, 17 | ringinvcl 17982 |
. . . . 5
  Unit  
              |
25 | 4, 22, 24 | syl2anc 673 |
. . . 4
    SubRing  

  
              |
26 | | issubdrg.i |
. . . . . 6
     |
27 | 2, 26, 18, 23 | subrginv 18102 |
. . . . 5
  SubRing 
Unit                 |
28 | 1, 22, 27 | syl2anc 673 |
. . . 4
    SubRing  

  
              |
29 | 25, 28, 10 | 3eltr4d 2564 |
. . 3
    SubRing  

  
      |
30 | 29 | ralrimiva 2809 |
. 2
  
SubRing              |
31 | 3 | ad2antlr 741 |
. . 3
  
SubRing   
          |
32 | | eqid 2471 |
. . . . . . . . . 10
Unit  Unit   |
33 | 2, 32, 18 | subrguss 18101 |
. . . . . . . . 9
 SubRing 
Unit 
Unit    |
34 | 33 | ad2antlr 741 |
. . . . . . . 8
  
SubRing   
        Unit 
Unit    |
35 | | eqid 2471 |
. . . . . . . . . . 11
         |
36 | 35, 32, 13 | isdrng 18057 |
. . . . . . . . . 10
  Unit           |
37 | 36 | simprbi 471 |
. . . . . . . . 9
 Unit      
   |
38 | 37 | ad2antrr 740 |
. . . . . . . 8
  
SubRing   
        Unit      
   |
39 | 34, 38 | sseqtrd 3454 |
. . . . . . 7
  
SubRing   
        Unit 
        |
40 | 17, 18 | unitss 17966 |
. . . . . . . 8
Unit       |
41 | 9 | ad2antlr 741 |
. . . . . . . 8
  
SubRing   
              |
42 | 40, 41 | syl5sseqr 3467 |
. . . . . . 7
  
SubRing   
        Unit 
  |
43 | 39, 42 | ssind 3647 |
. . . . . 6
  
SubRing   
        Unit 
     
    |
44 | 35 | subrgss 18087 |
. . . . . . . 8
 SubRing 
      |
45 | 44 | ad2antlr 741 |
. . . . . . 7
  
SubRing   
              |
46 | | difin2 3696 |
. . . . . . 7
    
       
    |
47 | 45, 46 | syl 17 |
. . . . . 6
  
SubRing   
                    |
48 | 43, 47 | sseqtr4d 3455 |
. . . . 5
  
SubRing   
        Unit 
    |
49 | 44 | ad2antlr 741 |
. . . . . . . . . . . 12
  
SubRing     
            |
50 | | simprl 772 |
. . . . . . . . . . . . . 14
  
SubRing     
          |
51 | 50, 6 | sylib 201 |
. . . . . . . . . . . . 13
  
SubRing     
         |
52 | 51 | simpld 466 |
. . . . . . . . . . . 12
  
SubRing     
        |
53 | 49, 52 | sseldd 3419 |
. . . . . . . . . . 11
  
SubRing     
            |
54 | 51 | simprd 470 |
. . . . . . . . . . 11
  
SubRing     
       |
55 | 35, 32, 13 | drngunit 18058 |
. . . . . . . . . . . 12
  Unit          |
56 | 55 | ad2antrr 740 |
. . . . . . . . . . 11
  
SubRing     
       Unit 
    
   |
57 | 53, 54, 56 | mpbir2and 936 |
. . . . . . . . . 10
  
SubRing     
      Unit    |
58 | | simprr 774 |
. . . . . . . . . 10
  
SubRing     
            |
59 | 2, 32, 18, 26 | subrgunit 18104 |
. . . . . . . . . . 11
 SubRing 
 Unit   Unit 
        |
60 | 59 | ad2antlr 741 |
. . . . . . . . . 10
  
SubRing     
       Unit 
 Unit 
        |
61 | 57, 52, 58, 60 | mpbir3and 1213 |
. . . . . . . . 9
  
SubRing     
      Unit    |
62 | 61 | expr 626 |
. . . . . . . 8
  
SubRing           Unit     |
63 | 62 | ralimdva 2805 |
. . . . . . 7
  SubRing  
 
       
   Unit     |
64 | 63 | imp 436 |
. . . . . 6
  
SubRing   
            Unit    |
65 | | dfss3 3408 |
. . . . . 6
  
Unit      Unit    |
66 | 64, 65 | sylibr 217 |
. . . . 5
  
SubRing   
          Unit    |
67 | 48, 66 | eqssd 3435 |
. . . 4
  
SubRing   
        Unit      |
68 | 14 | ad2antlr 741 |
. . . . . 6
  
SubRing   
       
      |
69 | 68 | sneqd 3971 |
. . . . 5
  
SubRing   
                |
70 | 41, 69 | difeq12d 3541 |
. . . 4
  
SubRing   
              
         |
71 | 67, 70 | eqtrd 2505 |
. . 3
  
SubRing   
        Unit                |
72 | 17, 18, 19 | isdrng 18057 |
. . 3
  Unit                 |
73 | 31, 71, 72 | sylanbrc 677 |
. 2
  
SubRing   
          |
74 | 30, 73 | impbida 850 |
1
  SubRing  
            |