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