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