Metamath Proof Explorer

Theorem iscph

Description: A subcomplex pre-Hilbert space is exactly a pre-Hilbert space over a subfield of the field of complex numbers closed under square roots of nonnegative reals equipped with a norm. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses iscph.v 
|- V = ( Base ` W )
iscph.h 
|- ., = ( .i ` W )
iscph.n 
|- N = ( norm ` W )
iscph.f 
|- F = ( Scalar ` W )
iscph.k 
|- K = ( Base ` F )
Assertion iscph 
|- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iscph.v 
 |-  V = ( Base ` W )
2 iscph.h 
 |-  ., = ( .i ` W )
3 iscph.n 
 |-  N = ( norm ` W )
4 iscph.f 
 |-  F = ( Scalar ` W )
5 iscph.k 
 |-  K = ( Base ` F )
6 elin 
 |-  ( W e. ( PreHil i^i NrmMod ) <-> ( W e. PreHil /\ W e. NrmMod ) )
7 6 anbi1i 
 |-  ( ( W e. ( PreHil i^i NrmMod ) /\ F = ( CCfld |`s K ) ) <-> ( ( W e. PreHil /\ W e. NrmMod ) /\ F = ( CCfld |`s K ) ) )
8 df-3an 
 |-  ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) <-> ( ( W e. PreHil /\ W e. NrmMod ) /\ F = ( CCfld |`s K ) ) )
9 7 8 bitr4i 
 |-  ( ( W e. ( PreHil i^i NrmMod ) /\ F = ( CCfld |`s K ) ) <-> ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) )
10 9 anbi1i 
 |-  ( ( ( W e. ( PreHil i^i NrmMod ) /\ F = ( CCfld |`s K ) ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) )
11 fvexd 
 |-  ( w = W -> ( Scalar ` w ) e. _V )
12 fvexd 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` f ) e. _V )
13 simplr 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = ( Scalar ` w ) )
14 simpll 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> w = W )
15 14 fveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Scalar ` w ) = ( Scalar ` W ) )
16 15 4 eqtr4di 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Scalar ` w ) = F )
17 13 16 eqtrd 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = F )
18 simpr 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = ( Base ` f ) )
19 17 fveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = ( Base ` F ) )
20 19 5 eqtr4di 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` f ) = K )
21 18 20 eqtrd 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = K )
22 21 oveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( CCfld |`s k ) = ( CCfld |`s K ) )
23 17 22 eqeq12d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( f = ( CCfld |`s k ) <-> F = ( CCfld |`s K ) ) )
24 21 ineq1d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( k i^i ( 0 [,) +oo ) ) = ( K i^i ( 0 [,) +oo ) ) )
25 24 imaeq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) = ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) )
26 25 21 sseq12d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k <-> ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K ) )
27 14 fveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = ( norm ` W ) )
28 27 3 eqtr4di 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( norm ` w ) = N )
29 14 fveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = ( Base ` W ) )
30 29 1 eqtr4di 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( Base ` w ) = V )
31 14 fveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ( .i ` W ) )
32 31 2 eqtr4di 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( .i ` w ) = ., )
33 32 oveqd 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( x ( .i ` w ) x ) = ( x ., x ) )
34 33 fveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( sqrt ` ( x ( .i ` w ) x ) ) = ( sqrt ` ( x ., x ) ) )
35 30 34 mpteq12dv 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
36 28 35 eqeq12d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) <-> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) )
37 23 26 36 3anbi123d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = ( CCfld |`s K ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) )
38 3anass 
 |-  ( ( F = ( CCfld |`s K ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) <-> ( F = ( CCfld |`s K ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) )
39 37 38 bitrdi 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = ( CCfld |`s K ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) ) )
40 12 39 sbcied 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = ( CCfld |`s K ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) ) )
41 11 40 sbcied 
 |-  ( w = W -> ( [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) <-> ( F = ( CCfld |`s K ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) ) )
42 df-cph 
 |-  CPreHil = { w e. ( PreHil i^i NrmMod ) | [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ ( sqrt " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) }
43 41 42 elrab2 
 |-  ( W e. CPreHil <-> ( W e. ( PreHil i^i NrmMod ) /\ ( F = ( CCfld |`s K ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) ) )
44 anass 
 |-  ( ( ( W e. ( PreHil i^i NrmMod ) /\ F = ( CCfld |`s K ) ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) <-> ( W e. ( PreHil i^i NrmMod ) /\ ( F = ( CCfld |`s K ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) ) )
45 43 44 bitr4i 
 |-  ( W e. CPreHil <-> ( ( W e. ( PreHil i^i NrmMod ) /\ F = ( CCfld |`s K ) ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) )
46 3anass 
 |-  ( ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) )
47 10 45 46 3bitr4i 
 |-  ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) )