Metamath Proof Explorer

Theorem osumclN

Description: Closure of orthogonal sum. If X and Y are orthogonal closed projective subspaces, then their sum is closed. (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcl.p 
|- .+ = ( +P ` K )
osumcl.o 
|- ._|_ = ( _|_P ` K )
osumcl.c 
|- C = ( PSubCl ` K )
Assertion osumclN 
|- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( X .+ Y ) e. C )

Proof

Step Hyp Ref Expression
1 osumcl.p 
 |-  .+ = ( +P ` K )
2 osumcl.o 
 |-  ._|_ = ( _|_P ` K )
3 osumcl.c 
 |-  C = ( PSubCl ` K )
4 simpl1 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> K e. HL )
5 simpl2 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> X e. C )
6 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 6 3 psubclssatN 
 |-  ( ( K e. HL /\ X e. C ) -> X C_ ( Atoms ` K ) )
8 4 5 7 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> X C_ ( Atoms ` K ) )
9 simpl3 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> Y e. C )
10 6 3 psubclssatN 
 |-  ( ( K e. HL /\ Y e. C ) -> Y C_ ( Atoms ` K ) )
11 4 9 10 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( Atoms ` K ) )
12 6 1 paddssat 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
13 4 8 11 12 syl3anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
14 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> K e. HL )
15 oveq1 
 |-  ( X = (/) -> ( X .+ Y ) = ( (/) .+ Y ) )
16 6 1 padd02 
 |-  ( ( K e. HL /\ Y C_ ( Atoms ` K ) ) -> ( (/) .+ Y ) = Y )
17 4 11 16 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( (/) .+ Y ) = Y )
18 15 17 sylan9eqr 
 |-  ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> ( X .+ Y ) = Y )
19 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> Y e. C )
20 18 19 eqeltrd 
 |-  ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> ( X .+ Y ) e. C )
21 2 3 psubcli2N 
 |-  ( ( K e. HL /\ ( X .+ Y ) e. C ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
22 14 20 21 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
23 1 2 3 osumcllem11N 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
24 23 anassrs 
 |-  ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X =/= (/) ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
25 24 eqcomd 
 |-  ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X =/= (/) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
26 22 25 pm2.61dane 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
27 6 2 3 ispsubclN 
 |-  ( K e. HL -> ( ( X .+ Y ) e. C <-> ( ( X .+ Y ) C_ ( Atoms ` K ) /\ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) ) ) )
28 4 27 syl 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( ( X .+ Y ) e. C <-> ( ( X .+ Y ) C_ ( Atoms ` K ) /\ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) ) ) )
29 13 26 28 mpbir2and 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( X .+ Y ) e. C )