This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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