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 ) )