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

Metamath Proof Explorer

Theorem paddasslem18

Description: Lemma for paddass . Combine paddasslem16 and paddasslem17 . (Contributed by NM, 12-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddass.a 
 |-  A = ( Atoms ` K )
2 paddass.p 
 |-  .+ = ( +P ` K )
3 eqid 
 |-  ( le ` K ) = ( le ` K )
4 eqid 
 |-  ( join ` K ) = ( join ` K )
5 3 4 1 2 paddasslem16 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )
6 5 3expa 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )
7 1 2 paddasslem17 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ -. ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )
8 7 3expa 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ -. ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )
9 6 8 pm2.61dan 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )