Metamath Proof Explorer

Theorem paddss1

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

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

Proof

Step Hyp Ref Expression
1 padd0.a 
 |-  A = ( Atoms ` K )
2 padd0.p 
 |-  .+ = ( +P ` K )
3 ssel 
 |-  ( X C_ Y -> ( p e. X -> p e. Y ) )
4 3 orim1d 
 |-  ( X C_ Y -> ( ( p e. X \/ p e. Z ) -> ( p e. Y \/ p e. Z ) ) )
5 ssrexv 
 |-  ( X C_ Y -> ( E. q e. X E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) -> E. q e. Y E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) )
6 5 anim2d 
 |-  ( X C_ Y -> ( ( p e. A /\ E. q e. X E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) -> ( p e. A /\ E. q e. Y E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) )
7 4 6 orim12d 
 |-  ( X C_ Y -> ( ( ( p e. X \/ p e. Z ) \/ ( p e. A /\ E. q e. X E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) -> ( ( p e. Y \/ p e. Z ) \/ ( p e. A /\ E. q e. Y E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
8 7 adantl 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( ( ( p e. X \/ p e. Z ) \/ ( p e. A /\ E. q e. X E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) -> ( ( p e. Y \/ p e. Z ) \/ ( p e. A /\ E. q e. Y E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
9 simpl1 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> K e. B )
10 sstr 
 |-  ( ( X C_ Y /\ Y C_ A ) -> X C_ A )
11 10 3ad2antr2 
 |-  ( ( X C_ Y /\ ( K e. B /\ Y C_ A /\ Z C_ A ) ) -> X C_ A )
12 11 ancoms 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> X C_ A )
13 simpl3 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> Z C_ A )
14 eqid 
 |-  ( le ` K ) = ( le ` K )
15 eqid 
 |-  ( join ` K ) = ( join ` K )
16 14 15 1 2 elpadd 
 |-  ( ( K e. B /\ X C_ A /\ Z C_ A ) -> ( p e. ( X .+ Z ) <-> ( ( p e. X \/ p e. Z ) \/ ( p e. A /\ E. q e. X E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
17 9 12 13 16 syl3anc 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( p e. ( X .+ Z ) <-> ( ( p e. X \/ p e. Z ) \/ ( p e. A /\ E. q e. X E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
18 14 15 1 2 elpadd 
 |-  ( ( K e. B /\ Y C_ A /\ Z C_ A ) -> ( p e. ( Y .+ Z ) <-> ( ( p e. Y \/ p e. Z ) \/ ( p e. A /\ E. q e. Y E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
19 18 adantr 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( p e. ( Y .+ Z ) <-> ( ( p e. Y \/ p e. Z ) \/ ( p e. A /\ E. q e. Y E. r e. Z p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
20 8 17 19 3imtr4d 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( p e. ( X .+ Z ) -> p e. ( Y .+ Z ) ) )
21 20 ssrdv 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( X .+ Z ) C_ ( Y .+ Z ) )
22 21 ex 
 |-  ( ( K e. B /\ Y C_ A /\ Z C_ A ) -> ( X C_ Y -> ( X .+ Z ) C_ ( Y .+ Z ) ) )