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 ) ) )`
` |-  +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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( 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 ) ) )`