Theorem paddss

Description: Subset law for projective subspace sum. ( unss analog.) (Contributed by NM, 7-Mar-2012)

	Ref	Expression
Hypotheses	paddss.a	|- A = ( Atoms ` K )
	paddss.s	|- S = ( PSubSp ` K )
	paddss.p	|- .+ = ( +P ` K )
Assertion	paddss	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( ( X C_ Z /\ Y C_ Z ) <-> ( X .+ Y ) C_ Z ) )

Proof

Step	Hyp	Ref	Expression
1		paddss.a	|- A = ( Atoms ` K )
2		paddss.s	|- S = ( PSubSp ` K )
3		paddss.p	|- .+ = ( +P ` K )
4		simpl	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> K e. B )
5		simpr1	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> X C_ A )
6		simpr2	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> Y C_ A )
7	1 2	psubssat	|- ( ( K e. B /\ Z e. S ) -> Z C_ A )
8	7	3ad2antr3	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> Z C_ A )
9	1 3	paddssw1	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X C_ Z /\ Y C_ Z ) -> ( X .+ Y ) C_ ( Z .+ Z ) ) )
10	4 5 6 8 9	syl13anc	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( ( X C_ Z /\ Y C_ Z ) -> ( X .+ Y ) C_ ( Z .+ Z ) ) )
11	2 3	paddidm	|- ( ( K e. B /\ Z e. S ) -> ( Z .+ Z ) = Z )
12	11	3ad2antr3	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( Z .+ Z ) = Z )
13	12	sseq2d	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( ( X .+ Y ) C_ ( Z .+ Z ) <-> ( X .+ Y ) C_ Z ) )
14	10 13	sylibd	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( ( X C_ Z /\ Y C_ Z ) -> ( X .+ Y ) C_ Z ) )
15	1 3	paddssw2	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) C_ Z -> ( X C_ Z /\ Y C_ Z ) ) )
16	4 5 6 8 15	syl13anc	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( ( X .+ Y ) C_ Z -> ( X C_ Z /\ Y C_ Z ) ) )
17	14 16	impbid	|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( ( X C_ Z /\ Y C_ Z ) <-> ( X .+ Y ) C_ Z ) )