# Metamath Proof Explorer

Description: A projective subspace sum is a superset of its second summand. ( ssun2 analog.) (Contributed by NM, 3-Jan-2012)

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

### Proof

Step Hyp Ref Expression
` |-  A = ( Atoms ` K )`
` |-  .+ = ( +P ` K )`
3 ssun2
` |-  X C_ ( Y u. X )`
4 ssun1
` |-  ( Y u. X ) C_ ( ( Y u. X ) u. { p e. A | E. q e. Y E. r e. X p ( le ` K ) ( q ( join ` K ) r ) } )`
5 3 4 sstri
` |-  X C_ ( ( Y u. X ) u. { p e. A | E. q e. Y E. r e. X p ( le ` K ) ( q ( join ` K ) r ) } )`
6 eqid
` |-  ( le ` K ) = ( le ` K )`
7 eqid
` |-  ( join ` K ) = ( join ` K )`
8 6 7 1 2 paddval
` |-  ( ( K e. B /\ Y C_ A /\ X C_ A ) -> ( Y .+ X ) = ( ( Y u. X ) u. { p e. A | E. q e. Y E. r e. X p ( le ` K ) ( q ( join ` K ) r ) } ) )`
9 8 3com23
` |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( Y .+ X ) = ( ( Y u. X ) u. { p e. A | E. q e. Y E. r e. X p ( le ` K ) ( q ( join ` K ) r ) } ) )`
10 5 9 sseqtrrid
` |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> X C_ ( Y .+ X ) )`