# Metamath Proof Explorer

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

Ref Expression
`|- A = ( Atoms ` K )`
`|- .+ = ( +P ` K )`
`|- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )`

### Proof

Step Hyp Ref Expression
` |-  A = ( Atoms ` K )`
` |-  .+ = ( +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 )`
` |-  ( ( 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 )`
` |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )`