Theorem osumclN 33578

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.)

Hypotheses

Ref	Expression
osumcl.p	|- .+ = ( +P ` K )
osumcl.o	|- ._|_ = ( _|_P ` K )
osumcl.c	|- C = ( PSubCl ` K )

Assertion

Ref	Expression
osumclN	|- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( X .+ Y ) e. C )

Proof of Theorem osumclN

Step	Hyp	Ref	Expression
1		simpl1 1017	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> K e. HL )
2		simpl2 1018	. . . 4 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> X e. C )
3		eqid 2462	. . . . 5 |- ( Atoms ` K ) = ( Atoms ` K )
4		osumcl.c	. . . . 5 |- C = ( PSubCl ` K )
5	3, 4	psubclssatN 33552	. . . 4 |- ( ( K e. HL /\ X e. C ) -> X C_ ( Atoms ` K ) )
6	1, 2, 5	syl2anc 671	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> X C_ ( Atoms ` K ) )
7		simpl3 1019	. . . 4 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> Y e. C )
8	3, 4	psubclssatN 33552	. . . 4 |- ( ( K e. HL /\ Y e. C ) -> Y C_ ( Atoms ` K ) )
9	1, 7, 8	syl2anc 671	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( Atoms ` K ) )
10		osumcl.p	. . . 4 |- .+ = ( +P ` K )
11	3, 10	paddssat 33425	. . 3 |- ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
12	1, 6, 9, 11	syl3anc 1276	. 2 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
13		simpll1 1053	. . . 4 |- ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> K e. HL )
14		oveq1 6327	. . . . . 6 |- ( X = (/) -> ( X .+ Y ) = ( (/) .+ Y ) )
15	3, 10	padd02 33423	. . . . . . 7 |- ( ( K e. HL /\ Y C_ ( Atoms ` K ) ) -> ( (/) .+ Y ) = Y )
16	1, 9, 15	syl2anc 671	. . . . . 6 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( (/) .+ Y ) = Y )
17	14, 16	sylan9eqr 2518	. . . . 5 |- ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> ( X .+ Y ) = Y )
18		simpll3 1055	. . . . 5 |- ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> Y e. C )
19	17, 18	eqeltrd 2540	. . . 4 |- ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> ( X .+ Y ) e. C )
20		osumcl.o	. . . . 5 |- ._|_ = ( _|_P ` K )
21	20, 4	psubcli2N 33550	. . . 4 |- ( ( K e. HL /\ ( X .+ Y ) e. C ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
22	13, 19, 21	syl2anc 671	. . 3 |- ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X = (/) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
23	10, 20, 4	osumcllem11N 33577	. . . . 5 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
24	23	anassrs 658	. . . 4 |- ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X =/= (/) ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
25	24	eqcomd 2468	. . 3 |- ( ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) /\ X =/= (/) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
26	22, 25	pm2.61dane 2723	. 2 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) )
27	3, 20, 4	ispsubclN 33548	. . 3 |- ( K e. HL -> ( ( X .+ Y ) e. C <-> ( ( X .+ Y ) C_ ( Atoms ` K ) /\ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( X .+ Y ) ) ) )
28	1, 27	syl 17	. 2 |- ( ( ( 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	12, 26, 28	mpbir2and 938	1 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( X .+ Y ) e. C )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   =/= wne 2633   C_ wss 3416   (/)c0 3743   ` cfv 5605  (class class class)co 6320   Atomscatm 32875   HLchlt 32962   +Pcpadd 33406   _|_PcpolN 33513   PSubClcpscN 33545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-riotaBAD 32571

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-1st 6825  df-2nd 6826  df-undef 7051  df-preset 16228  df-poset 16246  df-plt 16259  df-lub 16275  df-glb 16276  df-join 16277  df-meet 16278  df-p0 16340  df-p1 16341  df-lat 16347  df-clat 16409  df-oposet 32788  df-ol 32790  df-oml 32791  df-covers 32878  df-ats 32879  df-atl 32910  df-cvlat 32934  df-hlat 32963  df-psubsp 33114  df-pmap 33115  df-padd 33407  df-polarityN 33514  df-psubclN 33546

This theorem is referenced by:  pmapojoinN  33579  pexmidN  33580