Step | Hyp | Ref
| Expression |
1 | | elin 3628 |
. . . . 5
  NrmMod

NrmMod  |
2 | 1 | anbi1i 706 |
. . . 4
   NrmMod ℂfld ↾s    
NrmMod ℂfld ↾s     |
3 | | df-3an 993 |
. . . 4
  NrmMod ℂfld ↾s    
NrmMod ℂfld ↾s     |
4 | 2, 3 | bitr4i 260 |
. . 3
   NrmMod ℂfld ↾s    NrmMod ℂfld ↾s     |
5 | 4 | anbi1i 706 |
. 2
    NrmMod ℂfld ↾s                      
 
NrmMod ℂfld ↾s                         |
6 | | fvex 5897 |
. . . . . 6
Scalar   |
7 | 6 | a1i 11 |
. . . . 5
 Scalar    |
8 | | fvex 5897 |
. . . . . . 7
     |
9 | 8 | a1i 11 |
. . . . . 6
 
Scalar         |
10 | | simplr 767 |
. . . . . . . . . 10
   Scalar  
     Scalar    |
11 | | simpll 765 |
. . . . . . . . . . . 12
   Scalar  
    
  |
12 | 11 | fveq2d 5891 |
. . . . . . . . . . 11
   Scalar  
     Scalar  Scalar    |
13 | | iscph.f |
. . . . . . . . . . 11
Scalar   |
14 | 12, 13 | syl6eqr 2513 |
. . . . . . . . . 10
   Scalar  
     Scalar    |
15 | 10, 14 | eqtrd 2495 |
. . . . . . . . 9
   Scalar  
       |
16 | | simpr 467 |
. . . . . . . . . . 11
   Scalar  
           |
17 | 15 | fveq2d 5891 |
. . . . . . . . . . . 12
   Scalar  
               |
18 | | iscph.k |
. . . . . . . . . . . 12
     |
19 | 17, 18 | syl6eqr 2513 |
. . . . . . . . . . 11
   Scalar  
           |
20 | 16, 19 | eqtrd 2495 |
. . . . . . . . . 10
   Scalar  
       |
21 | 20 | oveq2d 6330 |
. . . . . . . . 9
   Scalar  
     ℂfld ↾s  ℂfld
↾s    |
22 | 15, 21 | eqeq12d 2476 |
. . . . . . . 8
   Scalar  
      ℂfld ↾s  ℂfld
↾s     |
23 | 20 | ineq1d 3644 |
. . . . . . . . . 10
   Scalar  
       
         |
24 | 23 | imaeq2d 5186 |
. . . . . . . . 9
   Scalar  
        
                |
25 | 24, 20 | sseq12d 3472 |
. . . . . . . 8
   Scalar  
         
    
     
      |
26 | 11 | fveq2d 5891 |
. . . . . . . . . 10
   Scalar  
               |
27 | | iscph.n |
. . . . . . . . . 10
     |
28 | 26, 27 | syl6eqr 2513 |
. . . . . . . . 9
   Scalar  
           |
29 | 11 | fveq2d 5891 |
. . . . . . . . . . 11
   Scalar  
               |
30 | | iscph.v |
. . . . . . . . . . 11
     |
31 | 29, 30 | syl6eqr 2513 |
. . . . . . . . . 10
   Scalar  
           |
32 | 11 | fveq2d 5891 |
. . . . . . . . . . . . 13
   Scalar  
               |
33 | | iscph.h |
. . . . . . . . . . . . 13
     |
34 | 32, 33 | syl6eqr 2513 |
. . . . . . . . . . . 12
   Scalar  
          |
35 | 34 | oveqd 6331 |
. . . . . . . . . . 11
   Scalar  
                 |
36 | 35 | fveq2d 5891 |
. . . . . . . . . 10
   Scalar  
                         |
37 | 31, 36 | mpteq12dv 4494 |
. . . . . . . . 9
   Scalar  
                                 |
38 | 28, 37 | eqeq12d 2476 |
. . . . . . . 8
   Scalar  
                           

   
      |
39 | 22, 25, 38 | 3anbi123d 1348 |
. . . . . . 7
   Scalar  
       ℂfld ↾s                                 
 ℂfld ↾s                       |
40 | | 3anass 995 |
. . . . . . 7
  ℂfld
↾s                   
 ℂfld ↾s                        |
41 | 39, 40 | syl6bb 269 |
. . . . . 6
   Scalar  
       ℂfld ↾s                                 
 ℂfld ↾s                         |
42 | 9, 41 | sbcied 3315 |
. . . . 5
 
Scalar          ![]. ].](_drbrack.gif)  ℂfld ↾s     
    
                      
 ℂfld ↾s                         |
43 | 7, 42 | sbcied 3315 |
. . . 4
   Scalar   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  ℂfld ↾s                                 
 ℂfld ↾s                         |
44 | | df-cph 22194 |
. . . 4
  NrmMod
 Scalar   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  ℂfld ↾s     
    
                         |
45 | 43, 44 | elrab2 3209 |
. . 3
   NrmMod 
ℂfld
↾s                         |
46 | | anass 659 |
. . 3
    NrmMod ℂfld ↾s                      
 
NrmMod 
ℂfld
↾s                         |
47 | 45, 46 | bitr4i 260 |
. 2
   
NrmMod ℂfld ↾s                         |
48 | | 3anass 995 |
. 2
   NrmMod
ℂfld ↾s                    
 
NrmMod ℂfld ↾s                         |
49 | 5, 47, 48 | 3bitr4i 285 |
1
   NrmMod ℂfld ↾s                       |