Metamath Proof Explorer

Theorem paddssw1

Description: Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012)

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

Proof

Step Hyp Ref Expression
1 paddssw.a 
 |-  A = ( Atoms ` K )
2 paddssw.p 
 |-  .+ = ( +P ` K )
3 simpl 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> K e. B )
4 simpr3 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Z C_ A )
5 1 2 paddss12 
 |-  ( ( K e. B /\ Z C_ A /\ Z C_ A ) -> ( ( X C_ Z /\ Y C_ Z ) -> ( X .+ Y ) C_ ( Z .+ Z ) ) )
6 3 4 4 5 syl3anc 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X C_ Z /\ Y C_ Z ) -> ( X .+ Y ) C_ ( Z .+ Z ) ) )