Metamath Proof Explorer

Theorem hlhil

Description: Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015)

Ref Expression
Assertion hlhil 
|- ( W e. CHil -> W e. Hil )

Proof

Step Hyp Ref Expression
1 hlphl 
 |-  ( W e. CHil -> W e. PreHil )
2 eqid 
 |-  ( proj ` W ) = ( proj ` W )
3 eqid 
 |-  ( ClSubSp ` W ) = ( ClSubSp ` W )
4 2 3 pjcss 
 |-  ( W e. PreHil -> dom ( proj ` W ) C_ ( ClSubSp ` W ) )
5 1 4 syl 
 |-  ( W e. CHil -> dom ( proj ` W ) C_ ( ClSubSp ` W ) )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 eqid 
 |-  ( TopOpen ` W ) = ( TopOpen ` W )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 6 7 8 3 cldcss2 
 |-  ( W e. CHil -> ( ClSubSp ` W ) = ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) )
10 elin 
 |-  ( x e. ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) <-> ( x e. ( LSubSp ` W ) /\ x e. ( Clsd ` ( TopOpen ` W ) ) ) )
11 7 8 2 pjth2 
 |-  ( ( W e. CHil /\ x e. ( LSubSp ` W ) /\ x e. ( Clsd ` ( TopOpen ` W ) ) ) -> x e. dom ( proj ` W ) )
12 11 3expib 
 |-  ( W e. CHil -> ( ( x e. ( LSubSp ` W ) /\ x e. ( Clsd ` ( TopOpen ` W ) ) ) -> x e. dom ( proj ` W ) ) )
13 10 12 syl5bi 
 |-  ( W e. CHil -> ( x e. ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) -> x e. dom ( proj ` W ) ) )
14 13 ssrdv 
 |-  ( W e. CHil -> ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) C_ dom ( proj ` W ) )
15 9 14 eqsstrd 
 |-  ( W e. CHil -> ( ClSubSp ` W ) C_ dom ( proj ` W ) )
16 5 15 eqssd 
 |-  ( W e. CHil -> dom ( proj ` W ) = ( ClSubSp ` W ) )
17 2 3 ishil 
 |-  ( W e. Hil <-> ( W e. PreHil /\ dom ( proj ` W ) = ( ClSubSp ` W ) ) )
18 1 16 17 sylanbrc 
 |-  ( W e. CHil -> W e. Hil )