Metamath Proof Explorer

Theorem ishil2

Description: The predicate "is a Hilbert space" (over a *-division ring). (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses ishil2.v 
|- V = ( Base ` H )
ishil2.s 
|- .(+) = ( LSSum ` H )
ishil2.o 
|- ._|_ = ( ocv ` H )
ishil2.c 
|- C = ( ClSubSp ` H )
Assertion ishil2 
|- ( H e. Hil <-> ( H e. PreHil /\ A. s e. C ( s .(+) ( ._|_ ` s ) ) = V ) )

Proof

Step Hyp Ref Expression
1 ishil2.v 
 |-  V = ( Base ` H )
2 ishil2.s 
 |-  .(+) = ( LSSum ` H )
3 ishil2.o 
 |-  ._|_ = ( ocv ` H )
4 ishil2.c 
 |-  C = ( ClSubSp ` H )
5 eqid 
 |-  ( proj ` H ) = ( proj ` H )
6 5 4 ishil 
 |-  ( H e. Hil <-> ( H e. PreHil /\ dom ( proj ` H ) = C ) )
7 5 4 pjcss 
 |-  ( H e. PreHil -> dom ( proj ` H ) C_ C )
8 eqss 
 |-  ( dom ( proj ` H ) = C <-> ( dom ( proj ` H ) C_ C /\ C C_ dom ( proj ` H ) ) )
9 8 baib 
 |-  ( dom ( proj ` H ) C_ C -> ( dom ( proj ` H ) = C <-> C C_ dom ( proj ` H ) ) )
10 7 9 syl 
 |-  ( H e. PreHil -> ( dom ( proj ` H ) = C <-> C C_ dom ( proj ` H ) ) )
11 dfss3 
 |-  ( C C_ dom ( proj ` H ) <-> A. s e. C s e. dom ( proj ` H ) )
12 10 11 bitrdi 
 |-  ( H e. PreHil -> ( dom ( proj ` H ) = C <-> A. s e. C s e. dom ( proj ` H ) ) )
13 eqid 
 |-  ( LSubSp ` H ) = ( LSubSp ` H )
14 4 13 csslss 
 |-  ( ( H e. PreHil /\ s e. C ) -> s e. ( LSubSp ` H ) )
15 1 13 3 2 5 pjdm2 
 |-  ( H e. PreHil -> ( s e. dom ( proj ` H ) <-> ( s e. ( LSubSp ` H ) /\ ( s .(+) ( ._|_ ` s ) ) = V ) ) )
16 15 baibd 
 |-  ( ( H e. PreHil /\ s e. ( LSubSp ` H ) ) -> ( s e. dom ( proj ` H ) <-> ( s .(+) ( ._|_ ` s ) ) = V ) )
17 14 16 syldan 
 |-  ( ( H e. PreHil /\ s e. C ) -> ( s e. dom ( proj ` H ) <-> ( s .(+) ( ._|_ ` s ) ) = V ) )
18 17 ralbidva 
 |-  ( H e. PreHil -> ( A. s e. C s e. dom ( proj ` H ) <-> A. s e. C ( s .(+) ( ._|_ ` s ) ) = V ) )
19 12 18 bitrd 
 |-  ( H e. PreHil -> ( dom ( proj ` H ) = C <-> A. s e. C ( s .(+) ( ._|_ ` s ) ) = V ) )
20 19 pm5.32i 
 |-  ( ( H e. PreHil /\ dom ( proj ` H ) = C ) <-> ( H e. PreHil /\ A. s e. C ( s .(+) ( ._|_ ` s ) ) = V ) )
21 6 20 bitri 
 |-  ( H e. Hil <-> ( H e. PreHil /\ A. s e. C ( s .(+) ( ._|_ ` s ) ) = V ) )