This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issh3

Description: Subspace H of a Hilbert space. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion issh3 
|- ( H C_ ~H -> ( H e. SH <-> ( 0h e. H /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) ) )

Proof

Step Hyp Ref Expression
1 issh2 
 |-  ( H e. SH <-> ( ( H C_ ~H /\ 0h e. H ) /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) )
2 anass 
 |-  ( ( ( H C_ ~H /\ 0h e. H ) /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) <-> ( H C_ ~H /\ ( 0h e. H /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) ) )
3 2 baib 
 |-  ( H C_ ~H -> ( ( ( H C_ ~H /\ 0h e. H ) /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) <-> ( 0h e. H /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) ) )
4 1 3 bitrid 
 |-  ( H C_ ~H -> ( H e. SH <-> ( 0h e. H /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) ) )