Metamath Proof Explorer

Theorem paddss12

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

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

Proof

Step Hyp Ref Expression
1 padd0.a 
 |-  A = ( Atoms ` K )
2 padd0.p 
 |-  .+ = ( +P ` K )
3 simpl1 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> K e. B )
4 simpl2 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> Y C_ A )
5 sstr 
 |-  ( ( Z C_ W /\ W C_ A ) -> Z C_ A )
6 5 ancoms 
 |-  ( ( W C_ A /\ Z C_ W ) -> Z C_ A )
7 6 ad2ant2l 
 |-  ( ( ( Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> Z C_ A )
8 7 3adantl1 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> Z C_ A )
9 3 4 8 3jca 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> ( K e. B /\ Y C_ A /\ Z C_ A ) )
10 simprl 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> X C_ Y )
11 1 2 paddss1 
 |-  ( ( K e. B /\ Y C_ A /\ Z C_ A ) -> ( X C_ Y -> ( X .+ Z ) C_ ( Y .+ Z ) ) )
12 9 10 11 sylc 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> ( X .+ Z ) C_ ( Y .+ Z ) )
13 1 2 paddss2 
 |-  ( ( K e. B /\ W C_ A /\ Y C_ A ) -> ( Z C_ W -> ( Y .+ Z ) C_ ( Y .+ W ) ) )
14 13 3com23 
 |-  ( ( K e. B /\ Y C_ A /\ W C_ A ) -> ( Z C_ W -> ( Y .+ Z ) C_ ( Y .+ W ) ) )
15 14 imp 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ Z C_ W ) -> ( Y .+ Z ) C_ ( Y .+ W ) )
16 15 adantrl 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> ( Y .+ Z ) C_ ( Y .+ W ) )
17 12 16 sstrd 
 |-  ( ( ( K e. B /\ Y C_ A /\ W C_ A ) /\ ( X C_ Y /\ Z C_ W ) ) -> ( X .+ Z ) C_ ( Y .+ W ) )
18 17 ex 
 |-  ( ( K e. B /\ Y C_ A /\ W C_ A ) -> ( ( X C_ Y /\ Z C_ W ) -> ( X .+ Z ) C_ ( Y .+ W ) ) )