Step | Hyp | Ref
| Expression |
1 | | elin 3796 |
. . . . 5
NrmMod
NrmMod |
2 | 1 | anbi1i 731 |
. . . 4
NrmMod ℂfld ↾s
NrmMod ℂfld ↾s |
3 | | df-3an 1039 |
. . . 4
NrmMod ℂfld ↾s
NrmMod ℂfld ↾s |
4 | 2, 3 | bitr4i 267 |
. . 3
NrmMod ℂfld ↾s NrmMod ℂfld ↾s |
5 | 4 | anbi1i 731 |
. 2
NrmMod ℂfld ↾s
NrmMod ℂfld ↾s |
6 | | fvexd 6203 |
. . . . 5
Scalar |
7 | | fvexd 6203 |
. . . . . 6
Scalar |
8 | | simplr 792 |
. . . . . . . . . 10
Scalar
Scalar |
9 | | simpll 790 |
. . . . . . . . . . . 12
Scalar
|
10 | 9 | fveq2d 6195 |
. . . . . . . . . . 11
Scalar
Scalar Scalar |
11 | | iscph.f |
. . . . . . . . . . 11
Scalar |
12 | 10, 11 | syl6eqr 2674 |
. . . . . . . . . 10
Scalar
Scalar |
13 | 8, 12 | eqtrd 2656 |
. . . . . . . . 9
Scalar
|
14 | | simpr 477 |
. . . . . . . . . . 11
Scalar
|
15 | 13 | fveq2d 6195 |
. . . . . . . . . . . 12
Scalar
|
16 | | iscph.k |
. . . . . . . . . . . 12
|
17 | 15, 16 | syl6eqr 2674 |
. . . . . . . . . . 11
Scalar
|
18 | 14, 17 | eqtrd 2656 |
. . . . . . . . . 10
Scalar
|
19 | 18 | oveq2d 6666 |
. . . . . . . . 9
Scalar
ℂfld ↾s ℂfld
↾s |
20 | 13, 19 | eqeq12d 2637 |
. . . . . . . 8
Scalar
ℂfld ↾s ℂfld
↾s |
21 | 18 | ineq1d 3813 |
. . . . . . . . . 10
Scalar
|
22 | 21 | imaeq2d 5466 |
. . . . . . . . 9
Scalar
|
23 | 22, 18 | sseq12d 3634 |
. . . . . . . 8
Scalar
|
24 | 9 | fveq2d 6195 |
. . . . . . . . . 10
Scalar
|
25 | | iscph.n |
. . . . . . . . . 10
|
26 | 24, 25 | syl6eqr 2674 |
. . . . . . . . 9
Scalar
|
27 | 9 | fveq2d 6195 |
. . . . . . . . . . 11
Scalar
|
28 | | iscph.v |
. . . . . . . . . . 11
|
29 | 27, 28 | syl6eqr 2674 |
. . . . . . . . . 10
Scalar
|
30 | 9 | fveq2d 6195 |
. . . . . . . . . . . . 13
Scalar
|
31 | | iscph.h |
. . . . . . . . . . . . 13
|
32 | 30, 31 | syl6eqr 2674 |
. . . . . . . . . . . 12
Scalar
|
33 | 32 | oveqd 6667 |
. . . . . . . . . . 11
Scalar
|
34 | 33 | fveq2d 6195 |
. . . . . . . . . 10
Scalar
|
35 | 29, 34 | mpteq12dv 4733 |
. . . . . . . . 9
Scalar
|
36 | 26, 35 | eqeq12d 2637 |
. . . . . . . 8
Scalar
|
37 | 20, 23, 36 | 3anbi123d 1399 |
. . . . . . 7
Scalar
ℂfld ↾s
ℂfld ↾s |
38 | | 3anass 1042 |
. . . . . . 7
ℂfld
↾s
ℂfld ↾s |
39 | 37, 38 | syl6bb 276 |
. . . . . 6
Scalar
ℂfld ↾s
ℂfld ↾s |
40 | 7, 39 | sbcied 3472 |
. . . . 5
Scalar ℂfld ↾s
ℂfld ↾s |
41 | 6, 40 | sbcied 3472 |
. . . 4
Scalar ℂfld ↾s
ℂfld ↾s |
42 | | df-cph 22968 |
. . . 4
NrmMod
Scalar ℂfld ↾s
|
43 | 41, 42 | elrab2 3366 |
. . 3
NrmMod
ℂfld
↾s |
44 | | anass 681 |
. . 3
NrmMod ℂfld ↾s
NrmMod
ℂfld
↾s |
45 | 43, 44 | bitr4i 267 |
. 2
NrmMod ℂfld ↾s |
46 | | 3anass 1042 |
. 2
NrmMod
ℂfld ↾s
NrmMod ℂfld ↾s |
47 | 5, 45, 46 | 3bitr4i 292 |
1
NrmMod ℂfld ↾s |