Metamath Proof Explorer

Theorem issh2

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. Definition of Beran p. 95. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 issh 
 |-  ( H e. SH <-> ( ( H C_ ~H /\ 0h e. H ) /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ H ) ) )
2 ax-hfvadd 
 |-  +h : ( ~H X. ~H ) --> ~H
3 ffun 
 |-  ( +h : ( ~H X. ~H ) --> ~H -> Fun +h )
4 2 3 ax-mp 
 |-  Fun +h
5 xpss12 
 |-  ( ( H C_ ~H /\ H C_ ~H ) -> ( H X. H ) C_ ( ~H X. ~H ) )
6 5 anidms 
 |-  ( H C_ ~H -> ( H X. H ) C_ ( ~H X. ~H ) )
7 2 fdmi 
 |-  dom +h = ( ~H X. ~H )
8 6 7 sseqtrrdi 
 |-  ( H C_ ~H -> ( H X. H ) C_ dom +h )
9 funimassov 
 |-  ( ( Fun +h /\ ( H X. H ) C_ dom +h ) -> ( ( +h " ( H X. H ) ) C_ H <-> A. x e. H A. y e. H ( x +h y ) e. H ) )
10 4 8 9 sylancr 
 |-  ( H C_ ~H -> ( ( +h " ( H X. H ) ) C_ H <-> A. x e. H A. y e. H ( x +h y ) e. H ) )
11 ax-hfvmul 
 |-  .h : ( CC X. ~H ) --> ~H
12 ffun 
 |-  ( .h : ( CC X. ~H ) --> ~H -> Fun .h )
13 11 12 ax-mp 
 |-  Fun .h
14 xpss2 
 |-  ( H C_ ~H -> ( CC X. H ) C_ ( CC X. ~H ) )
15 11 fdmi 
 |-  dom .h = ( CC X. ~H )
16 14 15 sseqtrrdi 
 |-  ( H C_ ~H -> ( CC X. H ) C_ dom .h )
17 funimassov 
 |-  ( ( Fun .h /\ ( CC X. H ) C_ dom .h ) -> ( ( .h " ( CC X. H ) ) C_ H <-> A. x e. CC A. y e. H ( x .h y ) e. H ) )
18 13 16 17 sylancr 
 |-  ( H C_ ~H -> ( ( .h " ( CC X. H ) ) C_ H <-> A. x e. CC A. y e. H ( x .h y ) e. H ) )
19 10 18 anbi12d 
 |-  ( H C_ ~H -> ( ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ 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 ) ) )
20 19 adantr 
 |-  ( ( H C_ ~H /\ 0h e. H ) -> ( ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. H ) ) C_ 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 ) ) )
21 20 pm5.32i 
 |-  ( ( ( H C_ ~H /\ 0h e. H ) /\ ( ( +h " ( H X. H ) ) C_ H /\ ( .h " ( CC X. 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 ) ) )
22 1 21 bitri 
 |-  ( 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 ) ) )