Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme1b Structured version   Visualization version   GIF version
Theorem cdleme1b 39400
Description: Part of proof of Lemma E in [Crawley] p. 113. Utility lemma showing 𝐹 is a lattice element. 𝐹 represents their f(r). (Contributed by NM, 6-Jun-2012.)
Hypotheses
Ref Expression
cdleme1.l ≀ = (leβ€˜πΎ)
cdleme1.j ∨ = (joinβ€˜πΎ)
cdleme1.m ∧ = (meetβ€˜πΎ)
cdleme1.a 𝐴 = (Atomsβ€˜πΎ)
cdleme1.h 𝐻 = (LHypβ€˜πΎ)
cdleme1.u π‘ˆ = ((𝑃 ∨ 𝑄) ∧ π‘Š)
cdleme1.f 𝐹 = ((𝑅 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ π‘Š)))
cdleme1.b 𝐡 = (Baseβ€˜πΎ)
Assertion
Ref Expression
cdleme1b (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝐹 ∈ 𝐡)
Proof of Theorem cdleme1b
StepHypRef Expression
1 cdleme1.f . 2 𝐹 = ((𝑅 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ π‘Š)))
2 hllat 38536 . . . 4 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
32ad2antrr 722 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝐾 ∈ Lat)
4 simpr3 1194 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝑅 ∈ 𝐴)
5 cdleme1.b . . . . . 6 𝐡 = (Baseβ€˜πΎ)
6 cdleme1.a . . . . . 6 𝐴 = (Atomsβ€˜πΎ)
75, 6atbase 38462 . . . . 5 (𝑅 ∈ 𝐴 β†’ 𝑅 ∈ 𝐡)
84, 7syl 17 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝑅 ∈ 𝐡)
9 cdleme1.l . . . . . 6 ≀ = (leβ€˜πΎ)
10 cdleme1.j . . . . . 6 ∨ = (joinβ€˜πΎ)
11 cdleme1.m . . . . . 6 ∧ = (meetβ€˜πΎ)
12 cdleme1.h . . . . . 6 𝐻 = (LHypβ€˜πΎ)
13 cdleme1.u . . . . . 6 π‘ˆ = ((𝑃 ∨ 𝑄) ∧ π‘Š)
149, 10, 11, 6, 12, 13, 5cdleme0aa 39384 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ π‘ˆ ∈ 𝐡)
15143adant3r3 1182 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ π‘ˆ ∈ 𝐡)
165, 10latjcl 18396 . . . 4 ((𝐾 ∈ Lat ∧ 𝑅 ∈ 𝐡 ∧ π‘ˆ ∈ 𝐡) β†’ (𝑅 ∨ π‘ˆ) ∈ 𝐡)
173, 8, 15, 16syl3anc 1369 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ (𝑅 ∨ π‘ˆ) ∈ 𝐡)
18 simpr2 1193 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝑄 ∈ 𝐴)
195, 6atbase 38462 . . . . 5 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ 𝐡)
2018, 19syl 17 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝑄 ∈ 𝐡)
21 simpr1 1192 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝑃 ∈ 𝐴)
225, 6atbase 38462 . . . . . . 7 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ 𝐡)
2321, 22syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝑃 ∈ 𝐡)
245, 10latjcl 18396 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐡 ∧ 𝑅 ∈ 𝐡) β†’ (𝑃 ∨ 𝑅) ∈ 𝐡)
253, 23, 8, 24syl3anc 1369 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ (𝑃 ∨ 𝑅) ∈ 𝐡)
265, 12lhpbase 39172 . . . . . 6 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ 𝐡)
2726ad2antlr 723 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ π‘Š ∈ 𝐡)
285, 11latmcl 18397 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ 𝐡 ∧ π‘Š ∈ 𝐡) β†’ ((𝑃 ∨ 𝑅) ∧ π‘Š) ∈ 𝐡)
293, 25, 27, 28syl3anc 1369 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ ((𝑃 ∨ 𝑅) ∧ π‘Š) ∈ 𝐡)
305, 10latjcl 18396 . . . 4 ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐡 ∧ ((𝑃 ∨ 𝑅) ∧ π‘Š) ∈ 𝐡) β†’ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ π‘Š)) ∈ 𝐡)
313, 20, 29, 30syl3anc 1369 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ π‘Š)) ∈ 𝐡)
325, 11latmcl 18397 . . 3 ((𝐾 ∈ Lat ∧ (𝑅 ∨ π‘ˆ) ∈ 𝐡 ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ π‘Š)) ∈ 𝐡) β†’ ((𝑅 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ π‘Š))) ∈ 𝐡)
333, 17, 31, 32syl3anc 1369 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ ((𝑅 ∨ π‘ˆ) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ π‘Š))) ∈ 𝐡)
341, 33eqeltrid 2835 1 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) β†’ 𝐹 ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  β€˜cfv 6542  (class class class)co 7411  Basecbs 17148  lecple 17208  joincjn 18268  meetcmee 18269  Latclat 18388  Atomscatm 38436  HLchlt 38523  LHypclh 39158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-lat 18389  df-ats 38440  df-atl 38471  df-cvlat 38495  df-hlat 38524  df-lhyp 39162
This theorem is referenced by:  cdleme3c  39404  cdleme4a  39413  cdleme5  39414  cdleme7e  39421  cdleme11  39444  cdleme15  39452  cdleme22gb  39468  cdleme19b  39478  cdleme19e  39481  cdleme20d  39486  cdleme20j  39492  cdleme20k  39493  cdleme20l2  39495  cdleme20l  39496  cdleme20m  39497  cdleme22e  39518  cdleme22eALTN  39519  cdleme22f  39520  cdleme27cl  39540  cdlemefr27cl  39577  cdleme35fnpq  39623
  Copyright terms: Public domain W3C validator