# Metamath Proof Explorer

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

Ref Expression
`|- A = ( Atoms ` K )`
`|- .+ = ( +P ` K )`
`|- ( ( K e. B /\ Y C_ A /\ Z C_ A ) -> ( X C_ Y -> ( X .+ Z ) C_ ( Y .+ Z ) ) )`

### Proof

Step Hyp Ref Expression
` |-  A = ( Atoms ` K )`
` |-  .+ = ( +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 ) ) ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( 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 ) ) ) ) )`
` |-  ( ( ( 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 ) ) ) ) )`
` |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( p e. ( X .+ Z ) -> p e. ( Y .+ Z ) ) )`
` |-  ( ( ( K e. B /\ Y C_ A /\ Z C_ A ) /\ X C_ Y ) -> ( X .+ Z ) C_ ( Y .+ Z ) )`
` |-  ( ( K e. B /\ Y C_ A /\ Z C_ A ) -> ( X C_ Y -> ( X .+ Z ) C_ ( Y .+ Z ) ) )`