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

Theorem cdlemi1 39270
Description: Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)
Hypotheses
Ref Expression
cdlemi.b 𝐵 = (Base‘𝐾)
cdlemi.l = (le‘𝐾)
cdlemi.j = (join‘𝐾)
cdlemi.m = (meet‘𝐾)
cdlemi.a 𝐴 = (Atoms‘𝐾)
cdlemi.h 𝐻 = (LHyp‘𝐾)
cdlemi.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemi.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemi.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
Assertion
Ref Expression
cdlemi1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐺)‘𝑃) (𝑃 (𝑅𝐺)))

Proof of Theorem cdlemi1
StepHypRef Expression
1 cdlemi.b . 2 𝐵 = (Base‘𝐾)
2 cdlemi.l . 2 = (le‘𝐾)
3 simp1l 1197 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ HL)
43hllatd 37815 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
5 simp1 1136 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
6 simp2l 1199 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑈𝐸)
7 simp2r 1200 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐺𝑇)
8 cdlemi.h . . . . 5 𝐻 = (LHyp‘𝐾)
9 cdlemi.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
10 cdlemi.e . . . . 5 𝐸 = ((TEndo‘𝐾)‘𝑊)
118, 9, 10tendocl 39219 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝐺𝑇) → (𝑈𝐺) ∈ 𝑇)
125, 6, 7, 11syl3anc 1371 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑈𝐺) ∈ 𝑇)
13 simp3l 1201 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
14 cdlemi.a . . . . 5 𝐴 = (Atoms‘𝐾)
151, 14atbase 37740 . . . 4 (𝑃𝐴𝑃𝐵)
1613, 15syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐵)
171, 8, 9ltrncl 38577 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐺) ∈ 𝑇𝑃𝐵) → ((𝑈𝐺)‘𝑃) ∈ 𝐵)
185, 12, 16, 17syl3anc 1371 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐺)‘𝑃) ∈ 𝐵)
19 cdlemi.r . . . . 5 𝑅 = ((trL‘𝐾)‘𝑊)
201, 8, 9, 19trlcl 38616 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐺) ∈ 𝑇) → (𝑅‘(𝑈𝐺)) ∈ 𝐵)
215, 12, 20syl2anc 584 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝑈𝐺)) ∈ 𝐵)
22 cdlemi.j . . . 4 = (join‘𝐾)
231, 22latjcl 18325 . . 3 ((𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ (𝑅‘(𝑈𝐺)) ∈ 𝐵) → (𝑃 (𝑅‘(𝑈𝐺))) ∈ 𝐵)
244, 16, 21, 23syl3anc 1371 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅‘(𝑈𝐺))) ∈ 𝐵)
251, 8, 9, 19trlcl 38616 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇) → (𝑅𝐺) ∈ 𝐵)
265, 7, 25syl2anc 584 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐺) ∈ 𝐵)
271, 22latjcl 18325 . . 3 ((𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ (𝑅𝐺) ∈ 𝐵) → (𝑃 (𝑅𝐺)) ∈ 𝐵)
284, 16, 26, 27syl3anc 1371 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅𝐺)) ∈ 𝐵)
291, 2, 22latlej2 18335 . . . 4 ((𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ((𝑈𝐺)‘𝑃) ∈ 𝐵) → ((𝑈𝐺)‘𝑃) (𝑃 ((𝑈𝐺)‘𝑃)))
304, 16, 18, 29syl3anc 1371 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐺)‘𝑃) (𝑃 ((𝑈𝐺)‘𝑃)))
31 cdlemi.m . . . . . . 7 = (meet‘𝐾)
322, 22, 31, 14, 8, 9, 19trlval2 38615 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐺) ∈ 𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝑈𝐺)) = ((𝑃 ((𝑈𝐺)‘𝑃)) 𝑊))
3312, 32syld3an2 1411 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝑈𝐺)) = ((𝑃 ((𝑈𝐺)‘𝑃)) 𝑊))
3433oveq2d 7370 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅‘(𝑈𝐺))) = (𝑃 ((𝑃 ((𝑈𝐺)‘𝑃)) 𝑊)))
351, 22latjcl 18325 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ((𝑈𝐺)‘𝑃) ∈ 𝐵) → (𝑃 ((𝑈𝐺)‘𝑃)) ∈ 𝐵)
364, 16, 18, 35syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 ((𝑈𝐺)‘𝑃)) ∈ 𝐵)
37 simp1r 1198 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
381, 8lhpbase 38450 . . . . . 6 (𝑊𝐻𝑊𝐵)
3937, 38syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐵)
401, 2, 22latlej1 18334 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ((𝑈𝐺)‘𝑃) ∈ 𝐵) → 𝑃 (𝑃 ((𝑈𝐺)‘𝑃)))
414, 16, 18, 40syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 (𝑃 ((𝑈𝐺)‘𝑃)))
421, 2, 22, 31, 14atmod3i1 38316 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 ((𝑈𝐺)‘𝑃)) ∈ 𝐵𝑊𝐵) ∧ 𝑃 (𝑃 ((𝑈𝐺)‘𝑃))) → (𝑃 ((𝑃 ((𝑈𝐺)‘𝑃)) 𝑊)) = ((𝑃 ((𝑈𝐺)‘𝑃)) (𝑃 𝑊)))
433, 13, 36, 39, 41, 42syl131anc 1383 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 ((𝑃 ((𝑈𝐺)‘𝑃)) 𝑊)) = ((𝑃 ((𝑈𝐺)‘𝑃)) (𝑃 𝑊)))
44 eqid 2736 . . . . . . . 8 (1.‘𝐾) = (1.‘𝐾)
452, 22, 44, 14, 8lhpjat2 38473 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
46453adant2 1131 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
4746oveq2d 7370 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 ((𝑈𝐺)‘𝑃)) (𝑃 𝑊)) = ((𝑃 ((𝑈𝐺)‘𝑃)) (1.‘𝐾)))
48 hlol 37812 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ OL)
493, 48syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ OL)
501, 31, 44olm11 37678 . . . . . 6 ((𝐾 ∈ OL ∧ (𝑃 ((𝑈𝐺)‘𝑃)) ∈ 𝐵) → ((𝑃 ((𝑈𝐺)‘𝑃)) (1.‘𝐾)) = (𝑃 ((𝑈𝐺)‘𝑃)))
5149, 36, 50syl2anc 584 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 ((𝑈𝐺)‘𝑃)) (1.‘𝐾)) = (𝑃 ((𝑈𝐺)‘𝑃)))
5247, 51eqtrd 2776 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 ((𝑈𝐺)‘𝑃)) (𝑃 𝑊)) = (𝑃 ((𝑈𝐺)‘𝑃)))
5334, 43, 523eqtrd 2780 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅‘(𝑈𝐺))) = (𝑃 ((𝑈𝐺)‘𝑃)))
5430, 53breqtrrd 5132 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐺)‘𝑃) (𝑃 (𝑅‘(𝑈𝐺))))
552, 8, 9, 19, 10tendotp 39213 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝐺𝑇) → (𝑅‘(𝑈𝐺)) (𝑅𝐺))
565, 6, 7, 55syl3anc 1371 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝑈𝐺)) (𝑅𝐺))
571, 2, 22latjlej2 18340 . . . 4 ((𝐾 ∈ Lat ∧ ((𝑅‘(𝑈𝐺)) ∈ 𝐵 ∧ (𝑅𝐺) ∈ 𝐵𝑃𝐵)) → ((𝑅‘(𝑈𝐺)) (𝑅𝐺) → (𝑃 (𝑅‘(𝑈𝐺))) (𝑃 (𝑅𝐺))))
584, 21, 26, 16, 57syl13anc 1372 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑅‘(𝑈𝐺)) (𝑅𝐺) → (𝑃 (𝑅‘(𝑈𝐺))) (𝑃 (𝑅𝐺))))
5956, 58mpd 15 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅‘(𝑈𝐺))) (𝑃 (𝑅𝐺)))
601, 2, 4, 18, 24, 28, 54, 59lattrd 18332 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐺)‘𝑃) (𝑃 (𝑅𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106   class class class wbr 5104  cfv 6494  (class class class)co 7354  Basecbs 17080  lecple 17137  joincjn 18197  meetcmee 18198  1.cp1 18310  Latclat 18317  OLcol 37625  Atomscatm 37714  HLchlt 37801  LHypclh 38436  LTrncltrn 38553  trLctrl 38610  TEndoctendo 39204
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-iin 4956  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5530  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7310  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7918  df-2nd 7919  df-map 8764  df-proset 18181  df-poset 18199  df-plt 18216  df-lub 18232  df-glb 18233  df-join 18234  df-meet 18235  df-p0 18311  df-p1 18312  df-lat 18318  df-clat 18385  df-oposet 37627  df-ol 37629  df-oml 37630  df-covers 37717  df-ats 37718  df-atl 37749  df-cvlat 37773  df-hlat 37802  df-psubsp 37955  df-pmap 37956  df-padd 38248  df-lhyp 38440  df-laut 38441  df-ldil 38556  df-ltrn 38557  df-trl 38611  df-tendo 39207
This theorem is referenced by:  cdlemi2  39271  cdlemi  39272
  Copyright terms: Public domain W3C validator