Step | Hyp | Ref
| Expression |
1 | | inss2 3653 |
. . 3
 
       |
2 | | minvec.x |
. . . 4
     |
3 | | minvec.m |
. . . 4
     |
4 | | minvec.n |
. . . 4
     |
5 | | minvec.u |
. . . 4
   |
6 | | minvec.y |
. . . 4
       |
7 | | minvec.w |
. . . 4
 
↾s  CMetSp |
8 | | minvec.a |
. . . 4
   |
9 | | minvec.j |
. . . 4
     |
10 | | minvec.r |
. . . 4
    
    |
11 | | minvec.s |
. . . 4
inf    |
12 | | minvec.d |
. . . 4
         |
13 | | minvec.f |
. . . 4
                   |
14 | | minvec.p |
. . . 4
        |
15 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | minveclem4a 22372 |
. . 3
  
        |
16 | 1, 15 | sseldi 3430 |
. 2
   |
17 | 12 | oveqi 6303 |
. . . . . . 7
                 |
18 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | minveclem4b 22373 |
. . . . . . . 8
   |
19 | 8, 18 | ovresd 6437 |
. . . . . . 7
                       |
20 | 17, 19 | syl5eq 2497 |
. . . . . 6
               |
21 | | cphngp 22151 |
. . . . . . . 8
 NrmGrp |
22 | 5, 21 | syl 17 |
. . . . . . 7

NrmGrp |
23 | | eqid 2451 |
. . . . . . . 8
         |
24 | 4, 2, 3, 23 | ngpds 21617 |
. . . . . . 7
  NrmGrp
                 |
25 | 22, 8, 18, 24 | syl3anc 1268 |
. . . . . 6
            
    |
26 | 20, 25 | eqtrd 2485 |
. . . . 5
             |
27 | 26 | adantr 467 |
. . . 4
 
             |
28 | | ngpms 21614 |
. . . . . . . 8
 NrmGrp   |
29 | 2, 12 | msmet 21472 |
. . . . . . . 8

      |
30 | 22, 28, 29 | 3syl 18 |
. . . . . . 7
       |
31 | | metcl 21347 |
. . . . . . 7
     
       |
32 | 30, 8, 18, 31 | syl3anc 1268 |
. . . . . 6
       |
33 | 32 | adantr 467 |
. . . . 5
 
       |
34 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | minveclem4c 22367 |
. . . . . 6
   |
35 | 34 | adantr 467 |
. . . . 5
 
   |
36 | 22 | adantr 467 |
. . . . . 6
 
 NrmGrp |
37 | | cphlmod 22152 |
. . . . . . . . 9
   |
38 | 5, 37 | syl 17 |
. . . . . . . 8
   |
39 | 38 | adantr 467 |
. . . . . . 7
 
   |
40 | 8 | adantr 467 |
. . . . . . 7
 
   |
41 | | eqid 2451 |
. . . . . . . . . 10
         |
42 | 2, 41 | lssss 18160 |
. . . . . . . . 9
    
  |
43 | 6, 42 | syl 17 |
. . . . . . . 8

  |
44 | 43 | sselda 3432 |
. . . . . . 7
 
   |
45 | 2, 3 | lmodvsubcl 18133 |
. . . . . . 7
 
     |
46 | 39, 40, 44, 45 | syl3anc 1268 |
. . . . . 6
 
     |
47 | 2, 4 | nmcl 21629 |
. . . . . 6
  NrmGrp
           |
48 | 36, 46, 47 | syl2anc 667 |
. . . . 5
 
         |
49 | 34, 32 | ltnled 9782 |
. . . . . . . 8
     
       |
50 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | minveclem3b 22370 |
. . . . . . . . . . . . . . . . . 18
       |
51 | | fbsspw 20847 |
. . . . . . . . . . . . . . . . . . . 20
    
   |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . 19

   |
53 | | sspwb 4649 |
. . . . . . . . . . . . . . . . . . . 20

    |
54 | 43, 53 | sylib 200 |
. . . . . . . . . . . . . . . . . . 19
     |
55 | 52, 54 | sstrd 3442 |
. . . . . . . . . . . . . . . . . 18

   |
56 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . 20
     |
57 | 2, 56 | eqeltri 2525 |
. . . . . . . . . . . . . . . . . . 19
 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   |
59 | | fbasweak 20880 |
. . . . . . . . . . . . . . . . . 18
              |
60 | 50, 55, 58, 59 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
       |
61 | 60 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
      |
62 | | fgcl 20893 |
. . . . . . . . . . . . . . . 16
    
          |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
 
    
          |
64 | | ssfg 20887 |
. . . . . . . . . . . . . . . . 17
    
      |
65 | 61, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
      |
66 | | minvec.t |
. . . . . . . . . . . . . . . . . . 19
                   |
67 | 32, 34 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
68 | 67 | rehalfcld 10859 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
69 | 68 | resqcld 12442 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
70 | 34 | resqcld 12442 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
71 | 69, 70 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
72 | 71 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                    |
73 | 34, 32, 34 | ltadd1d 10206 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           |
74 | 34 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
75 | 74 | 2timesd 10855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
76 | 75 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
         |
77 | | 2re 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
78 | | 2pos 10701 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
79 | 77, 78 | pm3.2i 457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
81 | | ltmuldiv2 10479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
        
           |
82 | 34, 67, 80, 81 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
           |
83 | 73, 76, 82 | 3bitr2d 285 |
. . . . . . . . . . . . . . . . . . . . . 22
     
           |
84 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | minveclem1 22366 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
   |
85 | 84 | simp3d 1022 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  |
86 | 84 | simp1d 1020 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
87 | 84 | simp2d 1021 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
88 | | 0re 9643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
89 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
90 | 89 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  

   |
91 | 90 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
   |
92 | 88, 85, 91 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
93 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
94 | | infregelb 10594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   

  
inf       |
95 | 86, 87, 92, 93, 94 | syl31anc 1271 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  inf   
   |
96 | 85, 95 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24

inf     |
97 | 96, 11 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
98 | | metge0 21360 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
       |
99 | 30, 8, 18, 98 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

      |
100 | 32, 34, 99, 97 | addge0d 10189 |
. . . . . . . . . . . . . . . . . . . . . . . 24

        |
101 | | divge0 10474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
         
          |
102 | 67, 100, 80, 101 | syl21anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . 23

          |
103 | 34, 68, 97, 102 | lt2sqd 12450 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
104 | 70, 69 | posdifd 10200 |
. . . . . . . . . . . . . . . . . . . . . 22
                                       |
105 | 83, 103, 104 | 3bitrd 283 |
. . . . . . . . . . . . . . . . . . . . 21
     
                     |
106 | 105 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                    |
107 | 72, 106 | elrpd 11338 |
. . . . . . . . . . . . . . . . . . 19
 
    
                    |
108 | 66, 107 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
109 | 6 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
    
      |
110 | | rabexg 4553 |
. . . . . . . . . . . . . . . . . . 19
    

                 |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
    

                 |
112 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19

                                    |
113 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . 21
               |
114 | 113 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . 20
         
     
                 |
115 | 114 | rabbidv 3036 |
. . . . . . . . . . . . . . . . . . 19
                                   |
116 | 112, 115 | elrnmpt1s 5082 |
. . . . . . . . . . . . . . . . . 18
          
       
                                    |
117 | 108, 111,
116 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
    

                                   |
118 | 117, 13 | syl6eleqr 2540 |
. . . . . . . . . . . . . . . 16
 
    

                 |
119 | 65, 118 | sseldd 3433 |
. . . . . . . . . . . . . . 15
 
    

                     |
120 | | ssrab2 3514 |
. . . . . . . . . . . . . . . 16
               |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . 15
 
    

               |
122 | 66 | oveq2i 6301 |
. . . . . . . . . . . . . . . . . . . 20
                               |
123 | 70 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
124 | 123 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . 21
               |
125 | 68 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
126 | 125 | resqcld 12442 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
127 | 126 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
128 | 124, 127 | pncan3d 9989 |
. . . . . . . . . . . . . . . . . . . 20
                                               |
129 | 122, 128 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . 19
                             |
130 | 129 | breq2d 4414 |
. . . . . . . . . . . . . . . . . 18
                 
     
                       |
131 | 30 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
               |
132 | 8 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
           |
133 | 44 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . 20
           |
134 | | metcl 21347 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
135 | 131, 132,
133, 134 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . 19
               |
136 | | metge0 21360 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
137 | 131, 132,
133, 136 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . 19
               |
138 | 102 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
                   |
139 | 135, 125,
137, 138 | le2sqd 12451 |
. . . . . . . . . . . . . . . . . 18
             
       
                       |
140 | 130, 139 | bitr4d 260 |
. . . . . . . . . . . . . . . . 17
                 
     
               |
141 | 140 | rabbidva 3035 |
. . . . . . . . . . . . . . . 16
 
    

                               |
142 | 43 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
  |
143 | | rabss2 3512 |
. . . . . . . . . . . . . . . . 17
                   
           |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    

                             |
145 | 141, 144 | eqsstrd 3466 |
. . . . . . . . . . . . . . 15
 
    

                   
           |
146 | | filss 20868 |
. . . . . . . . . . . . . . 15
         
         
               
                 
           
                               |
147 | 63, 119, 121, 145, 146 | syl13anc 1270 |
. . . . . . . . . . . . . 14
 
    

                   |
148 | | flimclsi 20993 |
. . . . . . . . . . . . . 14
     
            
     
                        |
149 | 147, 148 | syl 17 |
. . . . . . . . . . . . 13
 
    
     
                        |
150 | | inss1 3652 |
. . . . . . . . . . . . . . 15
 
             |
151 | 150, 15 | sseldi 3430 |
. . . . . . . . . . . . . 14
         |
152 | 151 | adantr 467 |
. . . . . . . . . . . . 13
 
    

       |
153 | 149, 152 | sseldd 3433 |
. . . . . . . . . . . 12
 
    
       
                |
154 | | ngpxms 21615 |
. . . . . . . . . . . . . . . . 17
 NrmGrp    |
155 | 2, 12 | xmsxmet 21471 |
. . . . . . . . . . . . . . . . 17
         |
156 | 22, 154, 155 | 3syl 18 |
. . . . . . . . . . . . . . . 16
        |
157 | 156 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
       |
158 | 8 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
  |
159 | 68 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
          |
160 | 159 | rexrd 9690 |
. . . . . . . . . . . . . . 15
 
    
          |
161 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
         |
162 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
                             |
163 | 161, 162 | blcld 21520 |
. . . . . . . . . . . . . . 15
                                        |
164 | 157, 158,
160, 163 | syl3anc 1268 |
. . . . . . . . . . . . . 14
 
    

                       |
165 | 9, 2, 12 | xmstopn 21466 |
. . . . . . . . . . . . . . . . 17
        |
166 | 22, 154, 165 | 3syl 18 |
. . . . . . . . . . . . . . . 16
       |
167 | 166 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
      |
168 | 167 | fveq2d 5869 |
. . . . . . . . . . . . . 14
 
    
              |
169 | 164, 168 | eleqtrrd 2532 |
. . . . . . . . . . . . 13
 
    

                   |
170 | | cldcls 20057 |
. . . . . . . . . . . . 13
     
            
                          
           |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . 12
 
    
                          
           |
172 | 153, 171 | eleqtrd 2531 |
. . . . . . . . . . 11
 
    
    
           |
173 | | oveq2 6298 |
. . . . . . . . . . . . . 14
           |
174 | 173 | breq1d 4412 |
. . . . . . . . . . . . 13
     
       
               |
175 | 174 | elrab 3196 |
. . . . . . . . . . . 12
              

               |
176 | 175 | simprbi 466 |
. . . . . . . . . . 11
                             |
177 | 172, 176 | syl 17 |
. . . . . . . . . 10
 
    
              |
178 | 32, 34, 32 | leadd2d 10208 |
. . . . . . . . . . . 12
                         |
179 | 32 | recnd 9669 |
. . . . . . . . . . . . . 14
       |
180 | 179 | 2timesd 10855 |
. . . . . . . . . . . . 13
                   |
181 | 180 | breq1d 4412 |
. . . . . . . . . . . 12
                       
         |
182 | | lemuldiv2 10487 |
. . . . . . . . . . . . . 14
              
            
               |
183 | 79, 182 | mp3an3 1353 |
. . . . . . . . . . . . 13
                                         |
184 | 32, 67, 183 | syl2anc 667 |
. . . . . . . . . . . 12
                 
           |
185 | 178, 181,
184 | 3bitr2d 285 |
. . . . . . . . . . 11
                     |
186 | 185 | biimpar 488 |
. . . . . . . . . 10
 
            
      |
187 | 177, 186 | syldan 473 |
. . . . . . . . 9
 
    
      |
188 | 187 | ex 436 |
. . . . . . . 8
         
   |
189 | 49, 188 | sylbird 239 |
. . . . . . 7
             |
190 | 189 | pm2.18d 115 |
. . . . . 6
    
  |
191 | 190 | adantr 467 |
. . . . 5
 
       |
192 | 86 | adantr 467 |
. . . . . . 7
 
   |
193 | 92 | adantr 467 |
. . . . . . 7
 
     |
194 | | simpr 463 |
. . . . . . . . 9
 
   |
195 | | fvex 5875 |
. . . . . . . . 9
       |
196 | | eqid 2451 |
. . . . . . . . . 10
            
    |
197 | 196 | elrnmpt1 5083 |
. . . . . . . . 9
                         |
198 | 194, 195,
197 | sylancl 668 |
. . . . . . . 8
 
           
     |
199 | 198, 10 | syl6eleqr 2540 |
. . . . . . 7
 
         |
200 | | infrelb 10596 |
. . . . . . 7
 


   
   inf  
        |
201 | 192, 193,
199, 200 | syl3anc 1268 |
. . . . . 6
 
 inf      
    |
202 | 11, 201 | syl5eqbr 4436 |
. . . . 5
 
         |
203 | 33, 35, 48, 191, 202 | letrd 9792 |
. . . 4
 
             |
204 | 27, 203 | eqbrtrrd 4425 |
. . 3
 
               |
205 | 204 | ralrimiva 2802 |
. 2
           
    |
206 | | oveq2 6298 |
. . . . . 6
       |
207 | 206 | fveq2d 5869 |
. . . . 5
               |
208 | 207 | breq1d 4412 |
. . . 4
           
     
 
         |
209 | 208 | ralbidv 2827 |
. . 3
  
         
            
     |
210 | 209 | rspcev 3150 |
. 2
            
   

              |
211 | 16, 205, 210 | syl2anc 667 |
1
  
         
    |