Metamath Proof Explorer

Theorem issh

Description: Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion issh 
|- ( H e. SH <-> ( ( H C_ ~H /\ 0h e. H ) /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 1 elpw2 
 |-  ( H e. ~P ~H <-> H C_ ~H )
3 3anass 
 |-  ( ( 0h e. H /\ ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) <-> ( 0h e. H /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) )
4 2 3 anbi12i 
 |-  ( ( H e. ~P ~H /\ ( 0h e. H /\ ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) <-> ( H C_ ~H /\ ( 0h e. H /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) ) )
5 eleq2 
 |-  ( h = H -> ( 0h e. h <-> 0h e. H ) )
6 id 
 |-  ( h = H -> h = H )
7 6 sqxpeqd 
 |-  ( h = H -> ( h X. h ) = ( H X. H ) )
8 7 imaeq2d 
 |-  ( h = H -> ( +h " ( h X. h ) ) = ( +h " ( H X. H ) ) )
9 8 6 sseq12d 
 |-  ( h = H -> ( ( +h " ( h X. h ) ) C_ h <-> ( +h " ( H X. H ) ) C_ H ) )
10 xpeq2 
 |-  ( h = H -> ( CC X. h ) = ( CC X. H ) )
11 10 imaeq2d 
 |-  ( h = H -> ( .h " ( CC X. h ) ) = ( .h " ( CC X. H ) ) )
12 11 6 sseq12d 
 |-  ( h = H -> ( ( .h " ( CC X. h ) ) C_ h <-> ( .h " ( CC X. H ) ) C_ H ) )
13 5 9 12 3anbi123d 
 |-  ( h = H -> ( ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h ) <-> ( 0h e. H /\ ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) )
14 df-sh 
 |-  SH = { h e. ~P ~H | ( 0h e. h /\ ( +h " ( h X. h ) ) C_ h /\ ( .h " ( CC X. h ) ) C_ h ) }
15 13 14 elrab2 
 |-  ( H e. SH <-> ( H e. ~P ~H /\ ( 0h e. H /\ ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) )
16 anass 
 |-  ( ( ( H C_ ~H /\ 0h e. H ) /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) <-> ( H C_ ~H /\ ( 0h e. H /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) ) )
17 4 15 16 3bitr4i 
 |-  ( H e. SH <-> ( ( H C_ ~H /\ 0h e. H ) /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) )