Metamath Proof Explorer

Theorem paddssw2

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 paddssw2 
|- ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) C_ Z -> ( X C_ Z /\ Y C_ Z ) ) )

Proof

Step Hyp Ref Expression
1 paddssw.a 
 |-  A = ( Atoms ` K )
2 paddssw.p 
 |-  .+ = ( +P ` K )
3 1 2 sspadd1 
 |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> X C_ ( X .+ Y ) )
4 3 3adant3r3 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> X C_ ( X .+ Y ) )
5 sstr 
 |-  ( ( X C_ ( X .+ Y ) /\ ( X .+ Y ) C_ Z ) -> X C_ Z )
6 4 5 sylan 
 |-  ( ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ ( X .+ Y ) C_ Z ) -> X C_ Z )
7 6 ex 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) C_ Z -> X C_ Z ) )
8 simpl 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> K e. B )
9 simpr2 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Y C_ A )
10 simpr1 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> X C_ A )
11 1 2 sspadd2 
 |-  ( ( K e. B /\ Y C_ A /\ X C_ A ) -> Y C_ ( X .+ Y ) )
12 8 9 10 11 syl3anc 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Y C_ ( X .+ Y ) )
13 sstr 
 |-  ( ( Y C_ ( X .+ Y ) /\ ( X .+ Y ) C_ Z ) -> Y C_ Z )
14 12 13 sylan 
 |-  ( ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ ( X .+ Y ) C_ Z ) -> Y C_ Z )
15 14 ex 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) C_ Z -> Y C_ Z ) )
16 7 15 jcad 
 |-  ( ( K e. B /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) C_ Z -> ( X C_ Z /\ Y C_ Z ) ) )