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 ) ) ) )