This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sspadd2

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

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

Proof

Step Hyp Ref Expression
1 padd0.a 
 |-  A = ( Atoms ` K )
2 padd0.p 
 |-  .+ = ( +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 ) )