Metamath Proof Explorer

Theorem paddssat

Description: A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012)

Ref Expression
Hypotheses padd0.a 
|- A = ( Atoms ` K )
padd0.p 
|- .+ = ( +P ` K )
Assertion paddssat 
|- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )

Proof

Step Hyp Ref Expression
1 padd0.a 
 |-  A = ( Atoms ` K )
2 padd0.p 
 |-  .+ = ( +P ` K )
3 eqid 
 |-  ( le ` K ) = ( le ` K )
4 eqid 
 |-  ( join ` K ) = ( join ` K )
5 3 4 1 2 paddval 
 |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) )
6 unss 
 |-  ( ( X C_ A /\ Y C_ A ) <-> ( X u. Y ) C_ A )
7 6 biimpi 
 |-  ( ( X C_ A /\ Y C_ A ) -> ( X u. Y ) C_ A )
8 ssrab2 
 |-  { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } C_ A
9 7 8 jctir 
 |-  ( ( X C_ A /\ Y C_ A ) -> ( ( X u. Y ) C_ A /\ { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } C_ A ) )
10 unss 
 |-  ( ( ( X u. Y ) C_ A /\ { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } C_ A ) <-> ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) C_ A )
11 9 10 sylib 
 |-  ( ( X C_ A /\ Y C_ A ) -> ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) C_ A )
12 11 3adant1 
 |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) C_ A )
13 5 12 eqsstrd 
 |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )