Metamath Proof Explorer

Theorem pjth

Description: Projection Theorem: Any Hilbert space vector A can be decomposed uniquely into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of Beran p. 102 (existence part). (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014)

Ref Expression
Hypotheses pjth.v 
|- V = ( Base ` W )
pjth.s 
|- .(+) = ( LSSum ` W )
pjth.o 
|- O = ( ocv ` W )
pjth.j 
|- J = ( TopOpen ` W )
pjth.l 
|- L = ( LSubSp ` W )
Assertion pjth 
|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> ( U .(+) ( O ` U ) ) = V )

Proof

Step Hyp Ref Expression
1 pjth.v 
 |-  V = ( Base ` W )
2 pjth.s 
 |-  .(+) = ( LSSum ` W )
3 pjth.o 
 |-  O = ( ocv ` W )
4 pjth.j 
 |-  J = ( TopOpen ` W )
5 pjth.l 
 |-  L = ( LSubSp ` W )
6 hlphl 
 |-  ( W e. CHil -> W e. PreHil )
7 6 3ad2ant1 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> W e. PreHil )
8 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
9 7 8 syl 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> W e. LMod )
10 simp2 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> U e. L )
11 1 5 lssss 
 |-  ( U e. L -> U C_ V )
12 11 3ad2ant2 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> U C_ V )
13 1 3 5 ocvlss 
 |-  ( ( W e. PreHil /\ U C_ V ) -> ( O ` U ) e. L )
14 7 12 13 syl2anc 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> ( O ` U ) e. L )
15 5 2 lsmcl 
 |-  ( ( W e. LMod /\ U e. L /\ ( O ` U ) e. L ) -> ( U .(+) ( O ` U ) ) e. L )
16 9 10 14 15 syl3anc 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> ( U .(+) ( O ` U ) ) e. L )
17 1 5 lssss 
 |-  ( ( U .(+) ( O ` U ) ) e. L -> ( U .(+) ( O ` U ) ) C_ V )
18 16 17 syl 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> ( U .(+) ( O ` U ) ) C_ V )
19 eqid 
 |-  ( norm ` W ) = ( norm ` W )
20 eqid 
 |-  ( +g ` W ) = ( +g ` W )
21 eqid 
 |-  ( -g ` W ) = ( -g ` W )
22 eqid 
 |-  ( .i ` W ) = ( .i ` W )
23 simpl1 
 |-  ( ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) /\ x e. V ) -> W e. CHil )
24 simpl2 
 |-  ( ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) /\ x e. V ) -> U e. L )
25 simpr 
 |-  ( ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) /\ x e. V ) -> x e. V )
26 simpl3 
 |-  ( ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) /\ x e. V ) -> U e. ( Clsd ` J ) )
27 1 19 20 21 22 5 23 24 25 4 2 3 26 pjthlem2 
 |-  ( ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) /\ x e. V ) -> x e. ( U .(+) ( O ` U ) ) )
28 18 27 eqelssd 
 |-  ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> ( U .(+) ( O ` U ) ) = V )