Metamath Proof Explorer

Theorem hhsssh

Description: The predicate " H is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1 
|- U = <. <. +h , .h >. , normh >.
hhsst.2 
|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
Assertion hhsssh 
|- ( H e. SH <-> ( W e. ( SubSp ` U ) /\ H C_ ~H ) )

Proof

Step Hyp Ref Expression
1 hhsst.1 
 |-  U = <. <. +h , .h >. , normh >.
2 hhsst.2 
 |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
3 1 2 hhsst 
 |-  ( H e. SH -> W e. ( SubSp ` U ) )
4 shss 
 |-  ( H e. SH -> H C_ ~H )
5 3 4 jca 
 |-  ( H e. SH -> ( W e. ( SubSp ` U ) /\ H C_ ~H ) )
6 eleq1 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( H e. SH <-> if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) e. SH ) )
7 eqid 
 |-  <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. = <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >.
8 xpeq1 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( H X. H ) = ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. H ) )
9 xpeq2 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. H ) = ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
10 8 9 eqtrd 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( H X. H ) = ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
11 10 reseq2d 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( +h |` ( H X. H ) ) = ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) )
12 xpeq2 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( CC X. H ) = ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
13 12 reseq2d 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( .h |` ( CC X. H ) ) = ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) )
14 11 13 opeq12d 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. = <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. )
15 reseq2 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( normh |` H ) = ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
16 14 15 opeq12d 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. = <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. )
17 2 16 syl5eq 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> W = <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. )
18 17 eleq1d 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( W e. ( SubSp ` U ) <-> <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. e. ( SubSp ` U ) ) )
19 sseq1 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( H C_ ~H <-> if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) C_ ~H ) )
20 18 19 anbi12d 
 |-  ( H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) <-> ( <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. e. ( SubSp ` U ) /\ if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) C_ ~H ) ) )
21 xpeq1 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( ~H X. ~H ) = ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. ~H ) )
22 xpeq2 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. ~H ) = ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
23 21 22 eqtrd 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( ~H X. ~H ) = ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
24 23 reseq2d 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( +h |` ( ~H X. ~H ) ) = ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) )
25 xpeq2 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( CC X. ~H ) = ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
26 25 reseq2d 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( .h |` ( CC X. ~H ) ) = ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) )
27 24 26 opeq12d 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. = <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. )
28 reseq2 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( normh |` ~H ) = ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) )
29 27 28 opeq12d 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> <. <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. , ( normh |` ~H ) >. = <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. )
30 29 eleq1d 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( <. <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. , ( normh |` ~H ) >. e. ( SubSp ` U ) <-> <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. e. ( SubSp ` U ) ) )
31 sseq1 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( ~H C_ ~H <-> if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) C_ ~H ) )
32 30 31 anbi12d 
 |-  ( ~H = if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) -> ( ( <. <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. , ( normh |` ~H ) >. e. ( SubSp ` U ) /\ ~H C_ ~H ) <-> ( <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. e. ( SubSp ` U ) /\ if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) C_ ~H ) ) )
33 ax-hfvadd 
 |-  +h : ( ~H X. ~H ) --> ~H
34 ffn 
 |-  ( +h : ( ~H X. ~H ) --> ~H -> +h Fn ( ~H X. ~H ) )
35 fnresdm 
 |-  ( +h Fn ( ~H X. ~H ) -> ( +h |` ( ~H X. ~H ) ) = +h )
36 33 34 35 mp2b 
 |-  ( +h |` ( ~H X. ~H ) ) = +h
37 ax-hfvmul 
 |-  .h : ( CC X. ~H ) --> ~H
38 ffn 
 |-  ( .h : ( CC X. ~H ) --> ~H -> .h Fn ( CC X. ~H ) )
39 fnresdm 
 |-  ( .h Fn ( CC X. ~H ) -> ( .h |` ( CC X. ~H ) ) = .h )
40 37 38 39 mp2b 
 |-  ( .h |` ( CC X. ~H ) ) = .h
41 36 40 opeq12i 
 |-  <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. = <. +h , .h >.
42 normf 
 |-  normh : ~H --> RR
43 ffn 
 |-  ( normh : ~H --> RR -> normh Fn ~H )
44 fnresdm 
 |-  ( normh Fn ~H -> ( normh |` ~H ) = normh )
45 42 43 44 mp2b 
 |-  ( normh |` ~H ) = normh
46 41 45 opeq12i 
 |-  <. <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. , ( normh |` ~H ) >. = <. <. +h , .h >. , normh >.
47 46 1 eqtr4i 
 |-  <. <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. , ( normh |` ~H ) >. = U
48 1 hhnv 
 |-  U e. NrmCVec
49 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
50 49 sspid 
 |-  ( U e. NrmCVec -> U e. ( SubSp ` U ) )
51 48 50 ax-mp 
 |-  U e. ( SubSp ` U )
52 47 51 eqeltri 
 |-  <. <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. , ( normh |` ~H ) >. e. ( SubSp ` U )
53 ssid 
 |-  ~H C_ ~H
54 52 53 pm3.2i 
 |-  ( <. <. ( +h |` ( ~H X. ~H ) ) , ( .h |` ( CC X. ~H ) ) >. , ( normh |` ~H ) >. e. ( SubSp ` U ) /\ ~H C_ ~H )
55 20 32 54 elimhyp 
 |-  ( <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. e. ( SubSp ` U ) /\ if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) C_ ~H )
56 55 simpli 
 |-  <. <. ( +h |` ( if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) , ( .h |` ( CC X. if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) ) >. , ( normh |` if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) ) >. e. ( SubSp ` U )
57 55 simpri 
 |-  if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) C_ ~H
58 1 7 56 57 hhshsslem2 
 |-  if ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) , H , ~H ) e. SH
59 6 58 dedth 
 |-  ( ( W e. ( SubSp ` U ) /\ H C_ ~H ) -> H e. SH )
60 5 59 impbii 
 |-  ( H e. SH <-> ( W e. ( SubSp ` U ) /\ H C_ ~H ) )