Theorem 2llnma1b 39571

Description: Generalization of 2llnma1 39572. (Contributed by NM, 26-Apr-2013.)

Hypotheses

Ref	Expression
2llnma1b.b	⊢ 𝐵 = (Base‘𝐾)
2llnma1b.l	⊢ ≤ = (le‘𝐾)
2llnma1b.j	⊢ ∨ = (join‘𝐾)
2llnma1b.m	⊢ ∧ = (meet‘𝐾)
2llnma1b.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
2llnma1b	⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) = 𝑃)

Proof of Theorem 2llnma1b

Step	Hyp	Ref	Expression
1		hllat 39147	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	3ad2ant1 1130	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝐾 ∈ Lat)
3		simp22 1204	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ∈ 𝐴)
4		2llnma1b.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
5		2llnma1b.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
6	4, 5	atbase 39073	. . . . . 6 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
7	3, 6	syl 17	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ∈ 𝐵)
8		simp21 1203	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑋 ∈ 𝐵)
9		2llnma1b.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
10		2llnma1b.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
11	4, 9, 10	latlej1 18487	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 𝑃 ≤ (𝑃 ∨ 𝑋))
12	2, 7, 8, 11	syl3anc 1368	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ≤ (𝑃 ∨ 𝑋))
13		simp23 1205	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑄 ∈ 𝐴)
14	4, 5	atbase 39073	. . . . . 6 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
15	13, 14	syl 17	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑄 ∈ 𝐵)
16	4, 9, 10	latlej1 18487	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → 𝑃 ≤ (𝑃 ∨ 𝑄))
17	2, 7, 15, 16	syl3anc 1368	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ≤ (𝑃 ∨ 𝑄))
18	4, 10	latjcl 18478	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑃 ∨ 𝑋) ∈ 𝐵)
19	2, 7, 8, 18	syl3anc 1368	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → (𝑃 ∨ 𝑋) ∈ 𝐵)
20		simp1 1133	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝐾 ∈ HL)
21	4, 10, 5	hlatjcl 39151	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵)
22	20, 3, 13, 21	syl3anc 1368	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → (𝑃 ∨ 𝑄) ∈ 𝐵)
23		2llnma1b.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
24	4, 9, 23	latlem12 18505	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ (𝑃 ∨ 𝑋) ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑃 ≤ (𝑃 ∨ 𝑋) ∧ 𝑃 ≤ (𝑃 ∨ 𝑄)) ↔ 𝑃 ≤ ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄))))
25	2, 7, 19, 22, 24	syl13anc 1369	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ≤ (𝑃 ∨ 𝑋) ∧ 𝑃 ≤ (𝑃 ∨ 𝑄)) ↔ 𝑃 ≤ ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄))))
26	12, 17, 25	mpbi2and 710	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ≤ ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)))
27		hlatl 39144	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
28	27	3ad2ant1 1130	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝐾 ∈ AtLat)
29		simp3 1135	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ¬ 𝑄 ≤ (𝑃 ∨ 𝑋))
30		nbrne2 5174	. . . . . 6 ⊢ ((𝑃 ≤ (𝑃 ∨ 𝑋) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ≠ 𝑄)
31	12, 29, 30	syl2anc 582	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ≠ 𝑄)
32	4, 10	latjcl 18478	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑋) ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → ((𝑃 ∨ 𝑋) ∨ 𝑄) ∈ 𝐵)
33	2, 19, 15, 32	syl3anc 1368	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∨ 𝑄) ∈ 𝐵)
34	4, 9, 10	latlej1 18487	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑋) ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑋) ≤ ((𝑃 ∨ 𝑋) ∨ 𝑄))
35	2, 19, 15, 34	syl3anc 1368	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → (𝑃 ∨ 𝑋) ≤ ((𝑃 ∨ 𝑋) ∨ 𝑄))
36	4, 9, 2, 7, 19, 33, 12, 35	lattrd 18485	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 ≤ ((𝑃 ∨ 𝑋) ∨ 𝑄))
37	4, 9, 10, 23, 5	cvrat3 39227	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑋) ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋) ∧ 𝑃 ≤ ((𝑃 ∨ 𝑋) ∨ 𝑄)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴))
38	37	3impia 1114	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑋) ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋) ∧ 𝑃 ≤ ((𝑃 ∨ 𝑋) ∨ 𝑄))) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴)
39	20, 19, 3, 13, 31, 29, 36, 38	syl133anc 1390	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴)
40	9, 5	atcmp 39095	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴) → (𝑃 ≤ ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) ↔ 𝑃 = ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄))))
41	28, 3, 39, 40	syl3anc 1368	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → (𝑃 ≤ ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) ↔ 𝑃 = ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄))))
42	26, 41	mpbid 231	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → 𝑃 = ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)))
43	42	eqcomd 2735	1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) = 𝑃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2100   ≠ wne 2933   class class class wbr 5154  ‘cfv 6557  (class class class)co 7428  Basecbs 17227  lecple 17287  joincjn 18350  meetcmee 18351  Latclat 18470  Atomscatm 39047  AtLatcal 39048  HLchlt 39134

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 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-rep 5291  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7749

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 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-rmo 3373  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-iun 5006  df-br 5155  df-opab 5217  df-mpt 5238  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6509  df-fun 6559  df-fn 6560  df-f 6561  df-f1 6562  df-fo 6563  df-f1o 6564  df-fv 6565  df-riota 7384  df-ov 7431  df-oprab 7432  df-proset 18334  df-poset 18352  df-plt 18369  df-lub 18385  df-glb 18386  df-join 18387  df-meet 18388  df-p0 18464  df-lat 18471  df-clat 18538  df-oposet 38960  df-ol 38962  df-oml 38963  df-covers 39050  df-ats 39051  df-atl 39082  df-cvlat 39106  df-hlat 39135

This theorem is referenced by:  2llnma1  39572  cdlemg4  40402  cdlemkfid1N  40706