Metamath Proof Explorer

Theorem paddss2

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

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

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 orim2d 
 |-  ( X C_ Y -> ( ( p e. Z \/ p e. X ) -> ( p e. Z \/ p e. Y ) ) )
5 ssrexv 
 |-  ( X C_ Y -> ( E. r e. X p ( le ` K ) ( q ( join ` K ) r ) -> E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) ) )
6 5 reximdv 
 |-  ( X C_ Y -> ( E. q e. Z E. r e. X p ( le ` K ) ( q ( join ` K ) r ) -> E. q e. Z E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) ) )
7 6 anim2d 
 |-  ( X C_ Y -> ( ( p e. A /\ E. q e. Z E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) -> ( p e. A /\ E. q e. Z E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) ) ) )
8 4 7 orim12d 
 |-  ( X C_ Y -> ( ( ( p e. Z \/ p e. X ) \/ ( p e. A /\ E. q e. Z E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) ) -> ( ( p e. Z \/ p e. Y ) \/ ( p e. A /\ E. q e. Z E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
9 8 adantl 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( ( ( p e. Z \/ p e. X ) \/ ( p e. A /\ E. q e. Z E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) ) -> ( ( p e. Z \/ p e. Y ) \/ ( p e. A /\ E. q e. Z E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
10 simpl1 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> K e. B )
11 simpl3 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> Z C_ A )
12 sstr 
 |-  ( ( X C_ Y /\ Y C_ A ) -> X C_ A )
13 12 3ad2antr2 
 |-  ( ( X C_ Y /\ ( K e. B /\ Y C_ A /\ Z C_ A ) ) -> X C_ A )
14 13 ancoms 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> X C_ A )
15 eqid 
 |-  ( le ` K ) = ( le ` K )
16 eqid 
 |-  ( join ` K ) = ( join ` K )
17 15 16 1 2 elpadd 
 |-  ( ( K e. B /\ Z C_ A /\ X C_ A ) -> ( p e. ( Z .+ X ) <-> ( ( p e. Z \/ p e. X ) \/ ( p e. A /\ E. q e. Z E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
18 10 11 14 17 syl3anc 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( p e. ( Z .+ X ) <-> ( ( p e. Z \/ p e. X ) \/ ( p e. A /\ E. q e. Z E. r e. X p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
19 simpl2 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> Y C_ A )
20 15 16 1 2 elpadd 
 |-  ( ( K e. B /\ Z C_ A /\ Y C_ A ) -> ( p e. ( Z .+ Y ) <-> ( ( p e. Z \/ p e. Y ) \/ ( p e. A /\ E. q e. Z E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
21 10 11 19 20 syl3anc 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( p e. ( Z .+ Y ) <-> ( ( p e. Z \/ p e. Y ) \/ ( p e. A /\ E. q e. Z E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
22 9 18 21 3imtr4d 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( p e. ( Z .+ X ) -> p e. ( Z .+ Y ) ) )
23 22 ssrdv 
 |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( Z .+ X ) C_ ( Z .+ Y ) )
24 23 ex 
 |-  ( ( K e. B /\ Y C_ A /\ Z C_ A ) -> ( X C_ Y -> ( Z .+ X ) C_ ( Z .+ Y ) ) )