Metamath Proof Explorer

Theorem chscl

Description: The subspace sum of two closed orthogonal spaces is closed. (Contributed by NM, 19-Oct-1999) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses chscl.1 
|- ( ph -> A e. CH )
chscl.2 
|- ( ph -> B e. CH )
chscl.3 
|- ( ph -> B C_ ( _|_ ` A ) )
Assertion chscl 
|- ( ph -> ( A +H B ) e. CH )

Proof

Step Hyp Ref Expression
1 chscl.1 
 |-  ( ph -> A e. CH )
2 chscl.2 
 |-  ( ph -> B e. CH )
3 chscl.3 
 |-  ( ph -> B C_ ( _|_ ` A ) )
4 chsh 
 |-  ( A e. CH -> A e. SH )
5 1 4 syl 
 |-  ( ph -> A e. SH )
6 chsh 
 |-  ( B e. CH -> B e. SH )
7 2 6 syl 
 |-  ( ph -> B e. SH )
8 shscl 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) e. SH )
9 5 7 8 syl2anc 
 |-  ( ph -> ( A +H B ) e. SH )
10 1 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> A e. CH )
11 2 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> B e. CH )
12 3 adantr 
 |-  ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> B C_ ( _|_ ` A ) )
13 simprl 
 |-  ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> f : NN --> ( A +H B ) )
14 simprr 
 |-  ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> f ~~>v z )
15 eqid 
 |-  ( x e. NN |-> ( ( projh ` A ) ` ( f ` x ) ) ) = ( x e. NN |-> ( ( projh ` A ) ` ( f ` x ) ) )
16 eqid 
 |-  ( x e. NN |-> ( ( projh ` B ) ` ( f ` x ) ) ) = ( x e. NN |-> ( ( projh ` B ) ` ( f ` x ) ) )
17 10 11 12 13 14 15 16 chscllem4 
 |-  ( ( ph /\ ( f : NN --> ( A +H B ) /\ f ~~>v z ) ) -> z e. ( A +H B ) )
18 17 ex 
 |-  ( ph -> ( ( f : NN --> ( A +H B ) /\ f ~~>v z ) -> z e. ( A +H B ) ) )
19 18 alrimivv 
 |-  ( ph -> A. f A. z ( ( f : NN --> ( A +H B ) /\ f ~~>v z ) -> z e. ( A +H B ) ) )
20 isch2 
 |-  ( ( A +H B ) e. CH <-> ( ( A +H B ) e. SH /\ A. f A. z ( ( f : NN --> ( A +H B ) /\ f ~~>v z ) -> z e. ( A +H B ) ) ) )
21 9 19 20 sylanbrc 
 |-  ( ph -> ( A +H B ) e. CH )