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

Theorem trljat2 37765
 Description: The value of a translation of an atom 𝑃 not under the fiducial co-atom 𝑊, joined with trace. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
Hypotheses
Ref Expression
trljat.l = (le‘𝐾)
trljat.j = (join‘𝐾)
trljat.a 𝐴 = (Atoms‘𝐾)
trljat.h 𝐻 = (LHyp‘𝐾)
trljat.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
trljat.r 𝑅 = ((trL‘𝐾)‘𝑊)
Assertion
Ref Expression
trljat2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) (𝑅𝐹)) = (𝑃 (𝐹𝑃)))

Proof of Theorem trljat2
StepHypRef Expression
1 simp1l 1194 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ HL)
2 trljat.l . . . . . 6 = (le‘𝐾)
3 trljat.a . . . . . 6 𝐴 = (Atoms‘𝐾)
4 trljat.h . . . . . 6 𝐻 = (LHyp‘𝐾)
5 trljat.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
62, 3, 4, 5ltrnat 37738 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃𝐴) → (𝐹𝑃) ∈ 𝐴)
763adant3r 1178 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) ∈ 𝐴)
81hllatd 36962 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
9 simp3l 1198 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
10 eqid 2758 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
1110, 3atbase 36887 . . . . . 6 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
129, 11syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 ∈ (Base‘𝐾))
13 simp1 1133 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
14 simp2 1134 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐹𝑇)
1510, 4, 5ltrncl 37723 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃 ∈ (Base‘𝐾)) → (𝐹𝑃) ∈ (Base‘𝐾))
1613, 14, 12, 15syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) ∈ (Base‘𝐾))
17 trljat.j . . . . . 6 = (join‘𝐾)
1810, 17latjcl 17727 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹𝑃) ∈ (Base‘𝐾)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
198, 12, 16, 18syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
20 simp1r 1195 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
2110, 4lhpbase 37596 . . . . 5 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2220, 21syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 ∈ (Base‘𝐾))
2310, 2, 17latlej2 17737 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹𝑃) ∈ (Base‘𝐾)) → (𝐹𝑃) (𝑃 (𝐹𝑃)))
248, 12, 16, 23syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) (𝑃 (𝐹𝑃)))
25 eqid 2758 . . . . 5 (meet‘𝐾) = (meet‘𝐾)
2610, 2, 17, 25, 3atmod2i1 37459 . . . 4 ((𝐾 ∈ HL ∧ ((𝐹𝑃) ∈ 𝐴 ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝐹𝑃) (𝑃 (𝐹𝑃))) → (((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊) (𝐹𝑃)) = ((𝑃 (𝐹𝑃))(meet‘𝐾)(𝑊 (𝐹𝑃))))
271, 7, 19, 22, 24, 26syl131anc 1380 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊) (𝐹𝑃)) = ((𝑃 (𝐹𝑃))(meet‘𝐾)(𝑊 (𝐹𝑃))))
282, 3, 4, 5ltrnel 37737 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
29 eqid 2758 . . . . . 6 (1.‘𝐾) = (1.‘𝐾)
302, 17, 29, 3, 4lhpjat1 37618 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊)) → (𝑊 (𝐹𝑃)) = (1.‘𝐾))
311, 20, 28, 30syl21anc 836 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑊 (𝐹𝑃)) = (1.‘𝐾))
3231oveq2d 7166 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐹𝑃))(meet‘𝐾)(𝑊 (𝐹𝑃))) = ((𝑃 (𝐹𝑃))(meet‘𝐾)(1.‘𝐾)))
33 hlol 36959 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ OL)
341, 33syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ OL)
3510, 25, 29olm11 36825 . . . 4 ((𝐾 ∈ OL ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃))(meet‘𝐾)(1.‘𝐾)) = (𝑃 (𝐹𝑃)))
3634, 19, 35syl2anc 587 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐹𝑃))(meet‘𝐾)(1.‘𝐾)) = (𝑃 (𝐹𝑃)))
3727, 32, 363eqtrrd 2798 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐹𝑃)) = (((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊) (𝐹𝑃)))
38 trljat.r . . . 4 𝑅 = ((trL‘𝐾)‘𝑊)
392, 17, 25, 3, 4, 5, 38trlval2 37761 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊))
4039oveq1d 7165 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑅𝐹) (𝐹𝑃)) = (((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊) (𝐹𝑃)))
4110, 4, 5, 38trlcl 37762 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) ∈ (Base‘𝐾))
4213, 14, 41syl2anc 587 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) ∈ (Base‘𝐾))
4310, 17latjcom 17735 . . 3 ((𝐾 ∈ Lat ∧ (𝑅𝐹) ∈ (Base‘𝐾) ∧ (𝐹𝑃) ∈ (Base‘𝐾)) → ((𝑅𝐹) (𝐹𝑃)) = ((𝐹𝑃) (𝑅𝐹)))
448, 42, 16, 43syl3anc 1368 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑅𝐹) (𝐹𝑃)) = ((𝐹𝑃) (𝑅𝐹)))
4537, 40, 443eqtr2rd 2800 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 5032  ‘cfv 6335  (class class class)co 7150  Basecbs 16541  lecple 16630  joincjn 17620  meetcmee 17621  1.cp1 17714  Latclat 17721  OLcol 36772  Atomscatm 36861  HLchlt 36948  LHypclh 37582  LTrncltrn 37699  trLctrl 37756 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 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-iun 4885  df-iin 4886  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7693  df-2nd 7694  df-map 8418  df-proset 17604  df-poset 17622  df-plt 17634  df-lub 17650  df-glb 17651  df-join 17652  df-meet 17653  df-p0 17715  df-p1 17716  df-lat 17722  df-clat 17784  df-oposet 36774  df-ol 36776  df-oml 36777  df-covers 36864  df-ats 36865  df-atl 36896  df-cvlat 36920  df-hlat 36949  df-psubsp 37101  df-pmap 37102  df-padd 37394  df-lhyp 37586  df-laut 37587  df-ldil 37702  df-ltrn 37703  df-trl 37757 This theorem is referenced by:  trljat3  37766  cdlemc3  37791
 Copyright terms: Public domain W3C validator