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

Metamath Proof Explorer

Theorem isch2

Description: Closed subspace H of a Hilbert space. Definition of Beran p. 107. (Contributed by NM, 17-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion isch2 
|- ( H e. CH <-> ( H e. SH /\ A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) )

Proof

Step Hyp Ref Expression
1 isch 
 |-  ( H e. CH <-> ( H e. SH /\ ( ~~>v " ( H ^m NN ) ) C_ H ) )
2 alcom 
 |-  ( A. f A. x ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> A. x A. f ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) )
3 19.23v 
 |-  ( A. f ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> ( E. f ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) )
4 vex 
 |-  x e. _V
5 4 elima2 
 |-  ( x e. ( ~~>v " ( H ^m NN ) ) <-> E. f ( f e. ( H ^m NN ) /\ f ~~>v x ) )
6 5 imbi1i 
 |-  ( ( x e. ( ~~>v " ( H ^m NN ) ) -> x e. H ) <-> ( E. f ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) )
7 3 6 bitr4i 
 |-  ( A. f ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> ( x e. ( ~~>v " ( H ^m NN ) ) -> x e. H ) )
8 7 albii 
 |-  ( A. x A. f ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> A. x ( x e. ( ~~>v " ( H ^m NN ) ) -> x e. H ) )
9 df-ss 
 |-  ( ( ~~>v " ( H ^m NN ) ) C_ H <-> A. x ( x e. ( ~~>v " ( H ^m NN ) ) -> x e. H ) )
10 8 9 bitr4i 
 |-  ( A. x A. f ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> ( ~~>v " ( H ^m NN ) ) C_ H )
11 2 10 bitri 
 |-  ( A. f A. x ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> ( ~~>v " ( H ^m NN ) ) C_ H )
12 nnex 
 |-  NN e. _V
13 elmapg 
 |-  ( ( H e. SH /\ NN e. _V ) -> ( f e. ( H ^m NN ) <-> f : NN --> H ) )
14 12 13 mpan2 
 |-  ( H e. SH -> ( f e. ( H ^m NN ) <-> f : NN --> H ) )
15 14 anbi1d 
 |-  ( H e. SH -> ( ( f e. ( H ^m NN ) /\ f ~~>v x ) <-> ( f : NN --> H /\ f ~~>v x ) ) )
16 15 imbi1d 
 |-  ( H e. SH -> ( ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) )
17 16 2albidv 
 |-  ( H e. SH -> ( A. f A. x ( ( f e. ( H ^m NN ) /\ f ~~>v x ) -> x e. H ) <-> A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) )
18 11 17 bitr3id 
 |-  ( H e. SH -> ( ( ~~>v " ( H ^m NN ) ) C_ H <-> A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) )
19 18 pm5.32i 
 |-  ( ( H e. SH /\ ( ~~>v " ( H ^m NN ) ) C_ H ) <-> ( H e. SH /\ A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) )
20 1 19 bitri 
 |-  ( H e. CH <-> ( H e. SH /\ A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) )