Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme10 Structured version   Visualization version   GIF version

Theorem cdleme10 37701
 Description: Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. 𝐷 represents s2. In their notation, we prove s ∨ s2 = s ∨ r. (Contributed by NM, 9-Jun-2012.)
Hypotheses
Ref Expression
cdleme10.l = (le‘𝐾)
cdleme10.j = (join‘𝐾)
cdleme10.m = (meet‘𝐾)
cdleme10.a 𝐴 = (Atoms‘𝐾)
cdleme10.h 𝐻 = (LHyp‘𝐾)
cdleme10.d 𝐷 = ((𝑅 𝑆) 𝑊)
Assertion
Ref Expression
cdleme10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑆 𝐷) = (𝑆 𝑅))

Proof of Theorem cdleme10
StepHypRef Expression
1 cdleme10.d . . 3 𝐷 = ((𝑅 𝑆) 𝑊)
21oveq2i 7156 . 2 (𝑆 𝐷) = (𝑆 ((𝑅 𝑆) 𝑊))
3 simp1l 1194 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝐾 ∈ HL)
4 simp3l 1198 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝑆𝐴)
5 simp2 1134 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝑅𝐴)
6 eqid 2798 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
7 cdleme10.j . . . . . 6 = (join‘𝐾)
8 cdleme10.a . . . . . 6 𝐴 = (Atoms‘𝐾)
96, 7, 8hlatjcl 36814 . . . . 5 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → (𝑅 𝑆) ∈ (Base‘𝐾))
103, 5, 4, 9syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑅 𝑆) ∈ (Base‘𝐾))
11 simp1r 1195 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝑊𝐻)
12 cdleme10.h . . . . . 6 𝐻 = (LHyp‘𝐾)
136, 12lhpbase 37445 . . . . 5 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
1411, 13syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝑊 ∈ (Base‘𝐾))
153hllatd 36811 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝐾 ∈ Lat)
166, 8atbase 36736 . . . . . 6 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
17163ad2ant2 1131 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝑅 ∈ (Base‘𝐾))
186, 8atbase 36736 . . . . . 6 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
194, 18syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝑆 ∈ (Base‘𝐾))
20 cdleme10.l . . . . . 6 = (le‘𝐾)
216, 20, 7latlej2 17683 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 (𝑅 𝑆))
2215, 17, 19, 21syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝑆 (𝑅 𝑆))
23 cdleme10.m . . . . 5 = (meet‘𝐾)
246, 20, 7, 23, 8atmod3i1 37311 . . . 4 ((𝐾 ∈ HL ∧ (𝑆𝐴 ∧ (𝑅 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑆 (𝑅 𝑆)) → (𝑆 ((𝑅 𝑆) 𝑊)) = ((𝑅 𝑆) (𝑆 𝑊)))
253, 4, 10, 14, 22, 24syl131anc 1380 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑆 ((𝑅 𝑆) 𝑊)) = ((𝑅 𝑆) (𝑆 𝑊)))
266, 7latjcom 17681 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑅 𝑆) = (𝑆 𝑅))
2715, 17, 19, 26syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑅 𝑆) = (𝑆 𝑅))
28 eqid 2798 . . . . . 6 (1.‘𝐾) = (1.‘𝐾)
2920, 7, 28, 8, 12lhpjat2 37468 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑆 𝑊) = (1.‘𝐾))
30293adant2 1128 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑆 𝑊) = (1.‘𝐾))
3127, 30oveq12d 7163 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → ((𝑅 𝑆) (𝑆 𝑊)) = ((𝑆 𝑅) (1.‘𝐾)))
32 hlol 36808 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ OL)
333, 32syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → 𝐾 ∈ OL)
346, 7latjcl 17673 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑆 𝑅) ∈ (Base‘𝐾))
3515, 19, 17, 34syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑆 𝑅) ∈ (Base‘𝐾))
366, 23, 28olm11 36674 . . . 4 ((𝐾 ∈ OL ∧ (𝑆 𝑅) ∈ (Base‘𝐾)) → ((𝑆 𝑅) (1.‘𝐾)) = (𝑆 𝑅))
3733, 35, 36syl2anc 587 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → ((𝑆 𝑅) (1.‘𝐾)) = (𝑆 𝑅))
3825, 31, 373eqtrd 2837 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑆 ((𝑅 𝑆) 𝑊)) = (𝑆 𝑅))
392, 38syl5eq 2845 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑅𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) → (𝑆 𝐷) = (𝑆 𝑅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   class class class wbr 5034  ‘cfv 6332  (class class class)co 7145  Basecbs 16495  lecple 16584  joincjn 17566  meetcmee 17567  1.cp1 17660  Latclat 17667  OLcol 36621  Atomscatm 36710  HLchlt 36797  LHypclh 37431 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-iun 4887  df-iin 4888  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7684  df-2nd 7685  df-proset 17550  df-poset 17568  df-plt 17580  df-lub 17596  df-glb 17597  df-join 17598  df-meet 17599  df-p0 17661  df-p1 17662  df-lat 17668  df-clat 17730  df-oposet 36623  df-ol 36625  df-oml 36626  df-covers 36713  df-ats 36714  df-atl 36745  df-cvlat 36769  df-hlat 36798  df-psubsp 36950  df-pmap 36951  df-padd 37243  df-lhyp 37435 This theorem is referenced by:  cdleme10tN  37705  cdleme20aN  37756  cdleme20g  37762
 Copyright terms: Public domain W3C validator