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 )