Metamath Proof Explorer

Theorem paddclN

Description: The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of MaedaMaeda p. 68. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddidm.s 
|- S = ( PSubSp ` K )
paddidm.p 
|- .+ = ( +P ` K )
Assertion paddclN 
|- ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )

Proof

Step Hyp Ref Expression
1 paddidm.s 
 |-  S = ( PSubSp ` K )
2 paddidm.p 
 |-  .+ = ( +P ` K )
3 simp1 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> K e. HL )
4 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
5 4 1 psubssat 
 |-  ( ( K e. HL /\ X e. S ) -> X C_ ( Atoms ` K ) )
6 5 3adant3 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> X C_ ( Atoms ` K ) )
7 4 1 psubssat 
 |-  ( ( K e. HL /\ Y e. S ) -> Y C_ ( Atoms ` K ) )
8 7 3adant2 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> Y C_ ( Atoms ` K ) )
9 4 2 paddssat 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
10 3 6 8 9 syl3anc 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
11 olc 
 |-  ( ( p e. ( Atoms ` K ) /\ E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) ) -> ( ( p e. ( X .+ Y ) \/ p e. ( X .+ Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) ) ) )
12 eqid 
 |-  ( le ` K ) = ( le ` K )
13 eqid 
 |-  ( join ` K ) = ( join ` K )
14 12 13 4 2 elpadd 
 |-  ( ( K e. HL /\ ( X .+ Y ) C_ ( Atoms ` K ) /\ ( X .+ Y ) C_ ( Atoms ` K ) ) -> ( p e. ( ( X .+ Y ) .+ ( X .+ Y ) ) <-> ( ( p e. ( X .+ Y ) \/ p e. ( X .+ Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
15 3 10 10 14 syl3anc 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( p e. ( ( X .+ Y ) .+ ( X .+ Y ) ) <-> ( ( p e. ( X .+ Y ) \/ p e. ( X .+ Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
16 4 2 padd4N 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) ) -> ( ( X .+ Y ) .+ ( X .+ Y ) ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
17 3 6 8 6 8 16 syl122anc 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( ( X .+ Y ) .+ ( X .+ Y ) ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
18 1 2 paddidm 
 |-  ( ( K e. HL /\ X e. S ) -> ( X .+ X ) = X )
19 18 3adant3 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( X .+ X ) = X )
20 1 2 paddidm 
 |-  ( ( K e. HL /\ Y e. S ) -> ( Y .+ Y ) = Y )
21 20 3adant2 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( Y .+ Y ) = Y )
22 19 21 oveq12d 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( ( X .+ X ) .+ ( Y .+ Y ) ) = ( X .+ Y ) )
23 17 22 eqtrd 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( ( X .+ Y ) .+ ( X .+ Y ) ) = ( X .+ Y ) )
24 23 eleq2d 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( p e. ( ( X .+ Y ) .+ ( X .+ Y ) ) <-> p e. ( X .+ Y ) ) )
25 15 24 bitr3d 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( ( ( p e. ( X .+ Y ) \/ p e. ( X .+ Y ) ) \/ ( p e. ( Atoms ` K ) /\ E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) ) ) <-> p e. ( X .+ Y ) ) )
26 11 25 syl5ib 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( ( p e. ( Atoms ` K ) /\ E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) ) -> p e. ( X .+ Y ) ) )
27 26 expd 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( p e. ( Atoms ` K ) -> ( E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) -> p e. ( X .+ Y ) ) ) )
28 27 ralrimiv 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> A. p e. ( Atoms ` K ) ( E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) -> p e. ( X .+ Y ) ) )
29 12 13 4 1 ispsubsp2 
 |-  ( K e. HL -> ( ( X .+ Y ) e. S <-> ( ( X .+ Y ) C_ ( Atoms ` K ) /\ A. p e. ( Atoms ` K ) ( E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) -> p e. ( X .+ Y ) ) ) ) )
30 29 3ad2ant1 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( ( X .+ Y ) e. S <-> ( ( X .+ Y ) C_ ( Atoms ` K ) /\ A. p e. ( Atoms ` K ) ( E. q e. ( X .+ Y ) E. r e. ( X .+ Y ) p ( le ` K ) ( q ( join ` K ) r ) -> p e. ( X .+ Y ) ) ) ) )
31 10 28 30 mpbir2and 
 |-  ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )