Theorem paddasslem16 34631

Description: Lemma for paddass 34634. Use elpaddn0 34596 to eliminate x and r from paddasslem15 34630. (Contributed by NM, 11-Jan-2012.)

Hypotheses

Ref	Expression
paddasslem.l	|- .<_ = ( le ` K )
paddasslem.j	|- .\/ = ( join ` K )
paddasslem.a	|- A = ( Atoms ` K )
paddasslem.p	|- .+ = ( +P ` K )

Assertion

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

Proof of Theorem paddasslem16

Dummy variables p r x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hllat 34160	. . . . 5 |- ( K e. HL -> K e. Lat )
2	1	3ad2ant1 1017	. . . 4 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> K e. Lat )
3		simp21 1029	. . . 4 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> X C_ A )
4		simp1 996	. . . . 5 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> K e. HL )
5		simp22 1030	. . . . 5 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> Y C_ A )
6		simp23 1031	. . . . 5 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> Z C_ A )
7		paddasslem.a	. . . . . 6 |- A = ( Atoms ` K )
8		paddasslem.p	. . . . . 6 |- .+ = ( +P ` K )
9	7, 8	paddssat 34610	. . . . 5 |- ( ( K e. HL /\ Y C_ A /\ Z C_ A ) -> ( Y .+ Z ) C_ A )
10	4, 5, 6, 9	syl3anc 1228	. . . 4 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( Y .+ Z ) C_ A )
11		simp3l 1024	. . . 4 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) )
12		paddasslem.l	. . . . 5 |- .<_ = ( le ` K )
13		paddasslem.j	. . . . 5 |- .\/ = ( join ` K )
14	12, 13, 7, 8	elpaddn0 34596	. . . 4 |- ( ( ( K e. Lat /\ X C_ A /\ ( Y .+ Z ) C_ A ) /\ ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) ) -> ( p e. ( X .+ ( Y .+ Z ) ) <-> ( p e. A /\ E. x e. X E. r e. ( Y .+ Z ) p .<_ ( x .\/ r ) ) ) )
15	2, 3, 10, 11, 14	syl31anc 1231	. . 3 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( p e. ( X .+ ( Y .+ Z ) ) <-> ( p e. A /\ E. x e. X E. r e. ( Y .+ Z ) p .<_ ( x .\/ r ) ) ) )
16		simpr 461	. . . . . . . 8 |- ( ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) -> ( Y =/= (/) /\ Z =/= (/) ) )
17	12, 13, 7, 8	paddasslem15 34630	. . . . . . . 8 |- ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
18	16, 17	syl3anl3 1278	. . . . . . 7 |- ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) /\ ( p e. A /\ ( x e. X /\ r e. ( Y .+ Z ) ) /\ p .<_ ( x .\/ r ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )
19	18	3exp2 1214	. . . . . 6 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( p e. A -> ( ( x e. X /\ r e. ( Y .+ Z ) ) -> ( p .<_ ( x .\/ r ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) ) )
20	19	imp 429	. . . . 5 |- ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) /\ p e. A ) -> ( ( x e. X /\ r e. ( Y .+ Z ) ) -> ( p .<_ ( x .\/ r ) -> p e. ( ( X .+ Y ) .+ Z ) ) ) )
21	20	rexlimdvv 2961	. . . 4 |- ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) /\ p e. A ) -> ( E. x e. X E. r e. ( Y .+ Z ) p .<_ ( x .\/ r ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
22	21	expimpd 603	. . 3 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( ( p e. A /\ E. x e. X E. r e. ( Y .+ Z ) p .<_ ( x .\/ r ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
23	15, 22	sylbid 215	. 2 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( p e. ( X .+ ( Y .+ Z ) ) -> p e. ( ( X .+ Y ) .+ Z ) ) )
24	23	ssrdv 3510	1 |- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   E.wrex 2815   C_ wss 3476   (/)c0 3785   class class class wbr 4447   ` cfv 5586  (class class class)co 6282   lecple 14558   joincjn 15427   Latclat 15528   Atomscatm 34060   HLchlt 34147   +Pcpadd 34591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-1st 6781  df-2nd 6782  df-poset 15429  df-plt 15441  df-lub 15457  df-glb 15458  df-join 15459  df-meet 15460  df-p0 15522  df-lat 15529  df-clat 15591  df-oposet 33973  df-ol 33975  df-oml 33976  df-covers 34063  df-ats 34064  df-atl 34095  df-cvlat 34119  df-hlat 34148  df-padd 34592

This theorem is referenced by:  paddasslem18  34633