Step | Hyp | Ref
| Expression |
1 | | inss1 3620 |
. . . . 5
NrmMod CMod NrmMod |
2 | 1 | sseli 3396 |
. . . 4
 NrmMod CMod
NrmMod |
3 | 1 | sseli 3396 |
. . . 4
 NrmMod CMod
NrmMod |
4 | | isnmhm 21778 |
. . . . 5
  NMHom    NrmMod NrmMod   LMHom 
 NGHom      |
5 | 4 | baib 916 |
. . . 4
  NrmMod
NrmMod
  NMHom    LMHom 
 NGHom      |
6 | 2, 3, 5 | syl2an 484 |
. . 3
  NrmMod CMod NrmMod CMod 
 NMHom    LMHom   NGHom      |
7 | 6 | 3adant3 1029 |
. 2
  NrmMod CMod NrmMod CMod
 
 NMHom    LMHom   NGHom      |
8 | | nmhmcn.j |
. . . . 5
     |
9 | | nmhmcn.k |
. . . . 5
     |
10 | 8, 9 | nghmcn 21777 |
. . . 4
  NGHom 

   |
11 | | simpll1 1048 |
. . . . . . . . . 10
    NrmMod
CMod NrmMod
CMod   LMHom      NrmMod
CMod  |
12 | 1, 11 | sseldi 3398 |
. . . . . . . . 9
    NrmMod
CMod NrmMod
CMod   LMHom      NrmMod |
13 | | nlmngp 21691 |
. . . . . . . . 9
 NrmMod NrmGrp |
14 | | ngpms 21625 |
. . . . . . . . 9
 NrmGrp   |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . 8
    NrmMod
CMod NrmMod
CMod   LMHom        |
16 | | msxms 21480 |
. . . . . . . 8

   |
17 | | eqid 2452 |
. . . . . . . . 9
         |
18 | | eqid 2452 |
. . . . . . . . 9
                                 |
19 | 17, 18 | xmsxmet 21482 |
. . . . . . . 8
                             |
20 | 15, 16, 19 | 3syl 18 |
. . . . . . 7
    NrmMod
CMod NrmMod
CMod   LMHom                                 |
21 | | simpr 467 |
. . . . . . . . 9
    NrmMod
CMod NrmMod
CMod   LMHom          |
22 | | simpll2 1049 |
. . . . . . . . . . . . . 14
    NrmMod
CMod NrmMod
CMod   LMHom      NrmMod
CMod  |
23 | 1, 22 | sseldi 3398 |
. . . . . . . . . . . . 13
    NrmMod
CMod NrmMod
CMod   LMHom      NrmMod |
24 | | nlmngp 21691 |
. . . . . . . . . . . . 13
 NrmMod NrmGrp |
25 | | ngpms 21625 |
. . . . . . . . . . . . 13
 NrmGrp   |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . . . . 12
    NrmMod
CMod NrmMod
CMod   LMHom        |
27 | | msxms 21480 |
. . . . . . . . . . . 12

   |
28 | | eqid 2452 |
. . . . . . . . . . . . 13
         |
29 | | eqid 2452 |
. . . . . . . . . . . . 13
                                 |
30 | 28, 29 | xmsxmet 21482 |
. . . . . . . . . . . 12
                             |
31 | 26, 27, 30 | 3syl 18 |
. . . . . . . . . . 11
    NrmMod
CMod NrmMod
CMod   LMHom                                 |
32 | | nlmlmod 21692 |
. . . . . . . . . . . 12
 NrmMod   |
33 | | eqid 2452 |
. . . . . . . . . . . . 13
         |
34 | 28, 33 | lmod0vcl 18131 |
. . . . . . . . . . . 12

          |
35 | 23, 32, 34 | 3syl 18 |
. . . . . . . . . . 11
    NrmMod
CMod NrmMod
CMod   LMHom                |
36 | | 1rp 11296 |
. . . . . . . . . . . 12
 |
37 | | rpxr 11299 |
. . . . . . . . . . . 12

  |
38 | 36, 37 | mp1i 13 |
. . . . . . . . . . 11
    NrmMod
CMod NrmMod
CMod   LMHom        |
39 | | eqid 2452 |
. . . . . . . . . . . 12
                                         |
40 | 39 | blopn 21526 |
. . . . . . . . . . 11
                                  

                                                  |
41 | 31, 35, 38, 40 | syl3anc 1271 |
. . . . . . . . . 10
    NrmMod
CMod NrmMod
CMod   LMHom                                                        |
42 | 9, 28, 29 | mstopn 21478 |
. . . . . . . . . . 11

                      |
43 | 23, 24, 25, 42 | 4syl 19 |
. . . . . . . . . 10
    NrmMod
CMod NrmMod
CMod   LMHom                            |
44 | 41, 43 | eleqtrrd 2533 |
. . . . . . . . 9
    NrmMod
CMod NrmMod
CMod   LMHom                                    |
45 | | cnima 20292 |
. . . . . . . . 9
                                                                    |
46 | 21, 44, 45 | syl2anc 671 |
. . . . . . . 8
    NrmMod
CMod NrmMod
CMod   LMHom                                         |
47 | 8, 17, 18 | mstopn 21478 |
. . . . . . . . 9

                      |
48 | 12, 13, 14, 47 | 4syl 19 |
. . . . . . . 8
    NrmMod
CMod NrmMod
CMod   LMHom                            |
49 | 46, 48 | eleqtrd 2532 |
. . . . . . 7
    NrmMod
CMod NrmMod
CMod   LMHom                                                             |
50 | | nlmlmod 21692 |
. . . . . . . . 9
 NrmMod   |
51 | | eqid 2452 |
. . . . . . . . . 10
         |
52 | 17, 51 | lmod0vcl 18131 |
. . . . . . . . 9

          |
53 | 12, 50, 52 | 3syl 18 |
. . . . . . . 8
    NrmMod
CMod NrmMod
CMod   LMHom                |
54 | | lmghm 18265 |
. . . . . . . . . . 11
  LMHom 

   |
55 | 54 | ad2antlr 738 |
. . . . . . . . . 10
    NrmMod
CMod NrmMod
CMod   LMHom          |
56 | 51, 33 | ghmid 16900 |
. . . . . . . . . 10
  
              |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
    NrmMod
CMod NrmMod
CMod   LMHom                    |
58 | 36 | a1i 11 |
. . . . . . . . . 10
    NrmMod
CMod NrmMod
CMod   LMHom        |
59 | | blcntr 21439 |
. . . . . . . . . 10
                                  

                                  |
60 | 31, 35, 58, 59 | syl3anc 1271 |
. . . . . . . . 9
    NrmMod
CMod NrmMod
CMod   LMHom                                        |
61 | 57, 60 | eqeltrd 2530 |
. . . . . . . 8
    NrmMod
CMod NrmMod
CMod   LMHom                                            |
62 | 17, 28 | lmhmf 18268 |
. . . . . . . . . 10
  LMHom 
              |
63 | 62 | ad2antlr 738 |
. . . . . . . . 9
    NrmMod
CMod NrmMod
CMod   LMHom                    |
64 | | ffn 5711 |
. . . . . . . . 9
            
      |
65 | | elpreima 5986 |
. . . . . . . . 9
    
                                              
                                        |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . 8
    NrmMod
CMod NrmMod
CMod   LMHom                                                                                             |
67 | 53, 61, 66 | mpbir2and 933 |
. . . . . . 7
    NrmMod
CMod NrmMod
CMod   LMHom                                             |
68 | | eqid 2452 |
. . . . . . . 8
                                         |
69 | 68 | mopni2 21519 |
. . . . . . 7
                                                                                                                                                                                      |
70 | 20, 49, 67, 69 | syl3anc 1271 |
. . . . . 6
    NrmMod
CMod NrmMod
CMod   LMHom                                                                      |
71 | | simpl1 1012 |
. . . . . . . . . . . . . . . . . . . 20
   NrmMod CMod
NrmMod
CMod   LMHom  
NrmMod CMod  |
72 | 1, 71 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . 19
   NrmMod CMod
NrmMod
CMod   LMHom  
NrmMod |
73 | 72, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   NrmMod CMod
NrmMod
CMod   LMHom  
NrmGrp |
74 | 73 | adantr 471 |
. . . . . . . . . . . . . . . . 17
    NrmMod
CMod NrmMod
CMod   LMHom      NrmGrp |
75 | 74 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
      NrmMod CMod NrmMod CMod
  LMHom            NrmGrp |
76 | | ngpgrp 21624 |
. . . . . . . . . . . . . . . 16
 NrmGrp   |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom              |
78 | | simpr 467 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom                  |
79 | | eqid 2452 |
. . . . . . . . . . . . . . . 16
         |
80 | | eqid 2452 |
. . . . . . . . . . . . . . . 16
         |
81 | 79, 17, 51, 80, 18 | nmval2 21617 |
. . . . . . . . . . . . . . 15
 
                                       |
82 | 77, 78, 81 | syl2anc 671 |
. . . . . . . . . . . . . 14
      NrmMod CMod NrmMod CMod
  LMHom                                              |
83 | 20 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom                                       |
84 | 53 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom                      |
85 | | xmetsym 21373 |
. . . . . . . . . . . . . . 15
                          
                                                               |
86 | 83, 78, 84, 85 | syl3anc 1271 |
. . . . . . . . . . . . . 14
      NrmMod CMod NrmMod CMod
  LMHom                                                              |
87 | 82, 86 | eqtrd 2486 |
. . . . . . . . . . . . 13
      NrmMod CMod NrmMod CMod
  LMHom                                              |
88 | 87 | breq1d 4384 |
. . . . . . . . . . . 12
      NrmMod CMod NrmMod CMod
  LMHom                                                |
89 | 88 | biimpd 212 |
. . . . . . . . . . 11
      NrmMod CMod NrmMod CMod
  LMHom                    
                           |
90 | 63 | ad2antrr 737 |
. . . . . . . . . . . . 13
      NrmMod CMod NrmMod CMod
  LMHom                          |
91 | | elpreima 5986 |
. . . . . . . . . . . . 13
    
                                      
                                    |
92 | 90, 64, 91 | 3syl 18 |
. . . . . . . . . . . 12
      NrmMod CMod NrmMod CMod
  LMHom                                                                                       |
93 | 31 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom                                       |
94 | 35 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom                      |
95 | 36, 37 | mp1i 13 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom              |
96 | | elbl 21414 |
. . . . . . . . . . . . . . 15
                                  

                                                                          |
97 | 93, 94, 95, 96 | syl3anc 1271 |
. . . . . . . . . . . . . 14
      NrmMod CMod NrmMod CMod
  LMHom                                            
        
                                |
98 | | simpl2 1013 |
. . . . . . . . . . . . . . . . . . . . . 22
   NrmMod CMod
NrmMod
CMod   LMHom  
NrmMod CMod  |
99 | 1, 98 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . 21
   NrmMod CMod
NrmMod
CMod   LMHom  
NrmMod |
100 | 99, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   NrmMod CMod
NrmMod
CMod   LMHom  
NrmGrp |
101 | 100 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
    NrmMod
CMod NrmMod
CMod   LMHom      NrmGrp |
102 | 101 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
      NrmMod CMod NrmMod CMod
  LMHom            NrmGrp |
103 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . 21
    NrmMod
CMod NrmMod
CMod   LMHom       LMHom    |
104 | 103 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
     NrmMod CMod
NrmMod CMod


LMHom      
 LMHom    |
105 | 104, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     NrmMod CMod
NrmMod CMod


LMHom      
              |
106 | 105 | ffvelrnda 6006 |
. . . . . . . . . . . . . . . . . 18
      NrmMod CMod NrmMod CMod
  LMHom                      |
107 | | eqid 2452 |
. . . . . . . . . . . . . . . . . . 19
         |
108 | 28, 107 | nmcl 21640 |
. . . . . . . . . . . . . . . . . 18
  NrmGrp
                       |
109 | 102, 106,
108 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
      NrmMod CMod NrmMod CMod
  LMHom                          |
110 | | 1re 9629 |
. . . . . . . . . . . . . . . . 17
 |
111 | | ltle 9709 |
. . . . . . . . . . . . . . . . 17
                           
           
   |
112 | 109, 110,
111 | sylancl 673 |
. . . . . . . . . . . . . . . 16
      NrmMod CMod NrmMod CMod
  LMHom                        
           
   |
113 | | ngpgrp 21624 |
. . . . . . . . . . . . . . . . . . . 20
 NrmGrp   |
114 | 102, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      NrmMod CMod NrmMod CMod
  LMHom              |
115 | | eqid 2452 |
. . . . . . . . . . . . . . . . . . . 20
         |
116 | 107, 28, 33, 115, 29 | nmval2 21617 |
. . . . . . . . . . . . . . . . . . 19
                                                     |
117 | 114, 106,
116 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
      NrmMod CMod NrmMod CMod
  LMHom                                                      |
118 | | xmetsym 21373 |
. . . . . . . . . . . . . . . . . . 19
                                  
        
                                                          |
119 | 93, 106, 94, 118 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . 18
      NrmMod CMod NrmMod CMod
  LMHom                                                                      |
120 | 117, 119 | eqtrd 2486 |
. . . . . . . . . . . . . . . . 17
      NrmMod CMod NrmMod CMod
  LMHom                                                      |
121 | 120 | breq1d 4384 |
. . . . . . . . . . . . . . . 16
      NrmMod CMod NrmMod CMod
  LMHom                                                        |
122 | | 1red 9645 |
. . . . . . . . . . . . . . . . 17
      NrmMod CMod NrmMod CMod
  LMHom              |
123 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
      NrmMod CMod NrmMod CMod
  LMHom              |
124 | 109, 122,
123 | lediv1d 11374 |
. . . . . . . . . . . . . . . 16
      NrmMod CMod NrmMod CMod
  LMHom                                      
     |
125 | 112, 121,
124 | 3imtr3d 275 |
. . . . . . . . . . . . . . 15
      NrmMod CMod NrmMod CMod
  LMHom                                                            |
126 | 125 | adantld 473 |
. . . . . . . . . . . . . 14
      NrmMod CMod NrmMod CMod
  LMHom                                                  
             
     |
127 | 97, 126 | sylbid 223 |
. . . . . . . . . . . . 13
      NrmMod CMod NrmMod CMod
  LMHom                                                                |
128 | 127 | adantld 473 |
. . . . . . . . . . . 12
      NrmMod CMod NrmMod CMod
  LMHom                                                                
     |
129 | 92, 128 | sylbid 223 |
. . . . . . . . . . 11
      NrmMod CMod NrmMod CMod
  LMHom                                                           
     |
130 | 89, 129 | imim12d 77 |
. . . . . . . . . 10
      NrmMod CMod NrmMod CMod
  LMHom                                     
                                 
                             |
131 | 130 | ralimdva 2786 |
. . . . . . . . 9
     NrmMod CMod
NrmMod CMod


LMHom      
 
                                                               
                                   |
132 | 20 | adantr 471 |
. . . . . . . . . . . 12
     NrmMod CMod
NrmMod CMod


LMHom      
                           |
133 | 53 | adantr 471 |
. . . . . . . . . . . 12
     NrmMod CMod
NrmMod CMod


LMHom      
          |
134 | | rpxr 11299 |
. . . . . . . . . . . . 13

  |
135 | 134 | adantl 472 |
. . . . . . . . . . . 12
     NrmMod CMod
NrmMod CMod


LMHom      
  |
136 | | blval 21412 |
. . . . . . . . . . . 12
                                  

                                                            |
137 | 132, 133,
135, 136 | syl3anc 1271 |
. . . . . . . . . . 11
     NrmMod CMod
NrmMod CMod


LMHom      
                                                            |
138 | 137 | sseq1d 3427 |
. . . . . . . . . 10
     NrmMod CMod
NrmMod CMod


LMHom      
                                                                                                                                |
139 | | rabss 3474 |
. . . . . . . . . 10
                                                                                              
                                    |
140 | 138, 139 | syl6bb 269 |
. . . . . . . . 9
     NrmMod CMod
NrmMod CMod


LMHom      
                                                              
                                                                   |
141 | | eqid 2452 |
. . . . . . . . . 10
         |
142 | | nmhmcn.g |
. . . . . . . . . 10
Scalar   |
143 | | nmhmcn.b |
. . . . . . . . . 10
     |
144 | 11 | adantr 471 |
. . . . . . . . . 10
     NrmMod CMod
NrmMod CMod


LMHom      
NrmMod
CMod  |
145 | 22 | adantr 471 |
. . . . . . . . . 10
     NrmMod CMod
NrmMod CMod


LMHom      
NrmMod
CMod  |
146 | | rpreccl 11316 |
. . . . . . . . . . . 12

    |
147 | 146 | adantl 472 |
. . . . . . . . . . 11
     NrmMod CMod
NrmMod CMod


LMHom      
    |
148 | 147 | rpxrd 11332 |
. . . . . . . . . 10
     NrmMod CMod
NrmMod CMod


LMHom      
    |
149 | | simpr 467 |
. . . . . . . . . 10
     NrmMod CMod
NrmMod CMod


LMHom      
  |
150 | | simpl3 1014 |
. . . . . . . . . . 11
   NrmMod CMod
NrmMod
CMod   LMHom  
  |
151 | 150 | ad2antrr 737 |
. . . . . . . . . 10
     NrmMod CMod
NrmMod CMod


LMHom      
  |
152 | 141, 17, 79, 107, 142, 143, 144, 145, 104, 148, 149, 151 | nmoleub2b 22143 |
. . . . . . . . 9
     NrmMod CMod
NrmMod CMod


LMHom      
                         
                    |
153 | 131, 140,
152 | 3imtr4d 276 |
. . . . . . . 8
     NrmMod CMod
NrmMod CMod


LMHom      
                                                                     
     |
154 | 74, 101, 55 | 3jca 1189 |
. . . . . . . . 9
    NrmMod
CMod NrmMod
CMod   LMHom      
NrmGrp NrmGrp
     |
155 | 146 | rpred 11331 |
. . . . . . . . 9

    |
156 | 141 | bddnghm 21742 |
. . . . . . . . . 10
   NrmGrp NrmGrp                    NGHom    |
157 | 156 | expr 624 |
. . . . . . . . 9
   NrmGrp NrmGrp                   NGHom     |
158 | 154, 155,
157 | syl2an 484 |
. . . . . . . 8
     NrmMod CMod
NrmMod CMod


LMHom      
          

NGHom     |
159 | 153, 158 | syld 45 |
. . . . . . 7
     NrmMod CMod
NrmMod CMod


LMHom      
                                                               NGHom     |
160 | 159 | rexlimdva 2852 |
. . . . . 6
    NrmMod
CMod NrmMod
CMod   LMHom       
                                                              NGHom     |
161 | 70, 160 | mpd 15 |
. . . . 5
    NrmMod
CMod NrmMod
CMod   LMHom       NGHom    |
162 | 161 | ex 440 |
. . . 4
   NrmMod CMod
NrmMod
CMod   LMHom  
  

NGHom     |
163 | 10, 162 | impbid2 209 |
. . 3
   NrmMod CMod
NrmMod
CMod   LMHom  
  NGHom       |
164 | 163 | pm5.32da 651 |
. 2
  NrmMod CMod NrmMod CMod
    LMHom 
 NGHom  
  LMHom        |
165 | 7, 164 | bitrd 261 |
1
  NrmMod CMod NrmMod CMod
 
 NMHom    LMHom        |