Theorem paddasslem16 39547

Description: Lemma for paddass 39550. Use elpaddn0 39512 to eliminate 𝑥 and 𝑟 from paddasslem15 39546. (Contributed by NM, 11-Jan-2012.)

Hypotheses

Ref	Expression
paddasslem.l	⊢ ≤ = (le‘𝐾)
paddasslem.j	⊢ ∨ = (join‘𝐾)
paddasslem.a	⊢ 𝐴 = (Atoms‘𝐾)
paddasslem.p	⊢ + = (+𝑃‘𝐾)

Assertion

Ref	Expression
paddasslem16	⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))

Proof of Theorem paddasslem16

Dummy variables 𝑝 𝑟 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hllat 39074	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	3ad2ant1 1130	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝐾 ∈ Lat)
3		simp21 1203	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝑋 ⊆ 𝐴)
4		simp1 1133	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝐾 ∈ HL)
5		simp22 1204	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝑌 ⊆ 𝐴)
6		simp23 1205	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → 𝑍 ⊆ 𝐴)
7		paddasslem.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
8		paddasslem.p	. . . . . 6 ⊢ + = (+𝑃‘𝐾)
9	7, 8	paddssat 39526	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 + 𝑍) ⊆ 𝐴)
10	4, 5, 6, 9	syl3anc 1368	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑌 + 𝑍) ⊆ 𝐴)
11		simp3l 1198	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅))
12		paddasslem.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
13		paddasslem.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
14	12, 13, 7, 8	elpaddn0 39512	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ (𝑌 + 𝑍) ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅)) → (𝑝 ∈ (𝑋 + (𝑌 + 𝑍)) ↔ (𝑝 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟))))
15	2, 3, 10, 11, 14	syl31anc 1370	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑝 ∈ (𝑋 + (𝑌 + 𝑍)) ↔ (𝑝 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟))))
16		simpr 483	. . . . . . . 8 ⊢ (((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) → (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))
17	12, 13, 7, 8	paddasslem15 39546	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
18	16, 17	syl3anl3 1411	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) ∧ (𝑝 ∈ 𝐴 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
19	18	3exp2 1351	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑝 ∈ 𝐴 → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) → (𝑝 ≤ (𝑥 ∨ 𝑟) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)))))
20	19	imp 405	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) ∧ 𝑝 ∈ 𝐴) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) → (𝑝 ≤ (𝑥 ∨ 𝑟) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))))
21	20	rexlimdvv 3201	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) ∧ 𝑝 ∈ 𝐴) → (∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)))
22	21	expimpd 452	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → ((𝑝 ∈ 𝐴 ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ (𝑌 + 𝑍)𝑝 ≤ (𝑥 ∨ 𝑟)) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)))
23	15, 22	sylbid 239	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑝 ∈ (𝑋 + (𝑌 + 𝑍)) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍)))
24	23	ssrdv 3984	1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2099   ≠ wne 2930  ∃wrex 3060   ⊆ wss 3946  ∅c0 4322   class class class wbr 5145  ‘cfv 6546  (class class class)co 7416  lecple 17268  joincjn 18331  Latclat 18451  Atomscatm 38974  HLchlt 39061  +_𝑃cpadd 39507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-iun 4995  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7995  df-2nd 7996  df-proset 18315  df-poset 18333  df-plt 18350  df-lub 18366  df-glb 18367  df-join 18368  df-meet 18369  df-p0 18445  df-lat 18452  df-clat 18519  df-oposet 38887  df-ol 38889  df-oml 38890  df-covers 38977  df-ats 38978  df-atl 39009  df-cvlat 39033  df-hlat 39062  df-padd 39508

This theorem is referenced by:  paddasslem18  39549