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

Theorem 4atexlemc 37327
Description: Lemma for 4atexlem7 37333. (Contributed by NM, 24-Nov-2012.)
Hypotheses
Ref Expression
4thatlem.ph (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑆𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ (𝑃 𝑅) = (𝑄 𝑅)) ∧ (𝑇𝐴 ∧ (𝑈 𝑇) = (𝑉 𝑇))) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))))
4thatlem0.l = (le‘𝐾)
4thatlem0.j = (join‘𝐾)
4thatlem0.m = (meet‘𝐾)
4thatlem0.a 𝐴 = (Atoms‘𝐾)
4thatlem0.h 𝐻 = (LHyp‘𝐾)
4thatlem0.u 𝑈 = ((𝑃 𝑄) 𝑊)
4thatlem0.v 𝑉 = ((𝑃 𝑆) 𝑊)
4thatlem0.c 𝐶 = ((𝑄 𝑇) (𝑃 𝑆))
Assertion
Ref Expression
4atexlemc (𝜑𝐶𝐴)

Proof of Theorem 4atexlemc
StepHypRef Expression
1 4thatlem0.c . . 3 𝐶 = ((𝑄 𝑇) (𝑃 𝑆))
2 4thatlem.ph . . . . 5 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑆𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ (𝑃 𝑅) = (𝑄 𝑅)) ∧ (𝑇𝐴 ∧ (𝑈 𝑇) = (𝑉 𝑇))) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))))
324atexlemkl 37315 . . . 4 (𝜑𝐾 ∈ Lat)
4 4thatlem0.j . . . . 5 = (join‘𝐾)
5 4thatlem0.a . . . . 5 𝐴 = (Atoms‘𝐾)
62, 4, 54atexlemqtb 37319 . . . 4 (𝜑 → (𝑄 𝑇) ∈ (Base‘𝐾))
72, 4, 54atexlempsb 37318 . . . 4 (𝜑 → (𝑃 𝑆) ∈ (Base‘𝐾))
8 eqid 2822 . . . . 5 (Base‘𝐾) = (Base‘𝐾)
9 4thatlem0.m . . . . 5 = (meet‘𝐾)
108, 9latmcom 17676 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
113, 6, 7, 10syl3anc 1368 . . 3 (𝜑 → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
121, 11syl5eq 2869 . 2 (𝜑𝐶 = ((𝑃 𝑆) (𝑄 𝑇)))
1324atexlemk 37305 . . 3 (𝜑𝐾 ∈ HL)
1424atexlemp 37308 . . 3 (𝜑𝑃𝐴)
1524atexlems 37310 . . 3 (𝜑𝑆𝐴)
1624atexlemq 37309 . . 3 (𝜑𝑄𝐴)
1724atexlemt 37311 . . 3 (𝜑𝑇𝐴)
18 4thatlem0.l . . . 4 = (le‘𝐾)
192, 18, 4, 54atexlempns 37320 . . 3 (𝜑𝑃𝑆)
20 4thatlem0.h . . . . 5 𝐻 = (LHyp‘𝐾)
21 4thatlem0.u . . . . 5 𝑈 = ((𝑃 𝑄) 𝑊)
22 4thatlem0.v . . . . 5 𝑉 = ((𝑃 𝑆) 𝑊)
232, 18, 4, 9, 5, 20, 21, 224atexlemntlpq 37326 . . . 4 (𝜑 → ¬ 𝑇 (𝑃 𝑄))
2418, 4, 5atnlej2 36638 . . . . 5 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑃𝐴𝑄𝐴) ∧ ¬ 𝑇 (𝑃 𝑄)) → 𝑇𝑄)
2524necomd 3066 . . . 4 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑃𝐴𝑄𝐴) ∧ ¬ 𝑇 (𝑃 𝑄)) → 𝑄𝑇)
2613, 17, 14, 16, 23, 25syl131anc 1380 . . 3 (𝜑𝑄𝑇)
2724atexlempnq 37313 . . . 4 (𝜑𝑃𝑄)
2824atexlemnslpq 37314 . . . 4 (𝜑 → ¬ 𝑆 (𝑃 𝑄))
2918, 4, 54atlem0ae 36852 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))) → ¬ 𝑄 (𝑃 𝑆))
3013, 14, 16, 15, 27, 28, 29syl132anc 1385 . . 3 (𝜑 → ¬ 𝑄 (𝑃 𝑆))
318, 5atbase 36547 . . . . 5 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
3217, 31syl 17 . . . 4 (𝜑𝑇 ∈ (Base‘𝐾))
332, 18, 4, 9, 5, 20, 214atexlemu 37322 . . . . 5 (𝜑𝑈𝐴)
342, 18, 4, 9, 5, 20, 21, 224atexlemv 37323 . . . . 5 (𝜑𝑉𝐴)
358, 4, 5hlatjcl 36625 . . . . 5 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴) → (𝑈 𝑉) ∈ (Base‘𝐾))
3613, 33, 34, 35syl3anc 1368 . . . 4 (𝜑 → (𝑈 𝑉) ∈ (Base‘𝐾))
378, 5atbase 36547 . . . . . 6 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
3816, 37syl 17 . . . . 5 (𝜑𝑄 ∈ (Base‘𝐾))
398, 4latjcl 17652 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
403, 7, 38, 39syl3anc 1368 . . . 4 (𝜑 → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
4124atexlemkc 37316 . . . . 5 (𝜑𝐾 ∈ CvLat)
422, 18, 4, 9, 5, 20, 21, 224atexlemunv 37324 . . . . 5 (𝜑𝑈𝑉)
4324atexlemutvt 37312 . . . . 5 (𝜑 → (𝑈 𝑇) = (𝑉 𝑇))
445, 18, 4cvlsupr4 36603 . . . . 5 ((𝐾 ∈ CvLat ∧ (𝑈𝐴𝑉𝐴𝑇𝐴) ∧ (𝑈𝑉 ∧ (𝑈 𝑇) = (𝑉 𝑇))) → 𝑇 (𝑈 𝑉))
4541, 33, 34, 17, 42, 43, 44syl132anc 1385 . . . 4 (𝜑𝑇 (𝑈 𝑉))
468, 4, 5hlatjcl 36625 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
4713, 14, 16, 46syl3anc 1368 . . . . . . . 8 (𝜑 → (𝑃 𝑄) ∈ (Base‘𝐾))
482, 204atexlemwb 37317 . . . . . . . 8 (𝜑𝑊 ∈ (Base‘𝐾))
498, 18, 9latmle1 17677 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑊) (𝑃 𝑄))
503, 47, 48, 49syl3anc 1368 . . . . . . 7 (𝜑 → ((𝑃 𝑄) 𝑊) (𝑃 𝑄))
5121, 50eqbrtrid 5077 . . . . . 6 (𝜑𝑈 (𝑃 𝑄))
528, 18, 9latmle1 17677 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑊) (𝑃 𝑆))
533, 7, 48, 52syl3anc 1368 . . . . . . 7 (𝜑 → ((𝑃 𝑆) 𝑊) (𝑃 𝑆))
5422, 53eqbrtrid 5077 . . . . . 6 (𝜑𝑉 (𝑃 𝑆))
558, 5atbase 36547 . . . . . . . 8 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
5633, 55syl 17 . . . . . . 7 (𝜑𝑈 ∈ (Base‘𝐾))
578, 5atbase 36547 . . . . . . . 8 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
5834, 57syl 17 . . . . . . 7 (𝜑𝑉 ∈ (Base‘𝐾))
598, 18, 4latjlej12 17668 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) ∧ (𝑉 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾))) → ((𝑈 (𝑃 𝑄) ∧ 𝑉 (𝑃 𝑆)) → (𝑈 𝑉) ((𝑃 𝑄) (𝑃 𝑆))))
603, 56, 47, 58, 7, 59syl122anc 1376 . . . . . 6 (𝜑 → ((𝑈 (𝑃 𝑄) ∧ 𝑉 (𝑃 𝑆)) → (𝑈 𝑉) ((𝑃 𝑄) (𝑃 𝑆))))
6151, 54, 60mp2and 698 . . . . 5 (𝜑 → (𝑈 𝑉) ((𝑃 𝑄) (𝑃 𝑆)))
624, 5hlatjass 36628 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
6313, 14, 16, 15, 62syl13anc 1369 . . . . . 6 (𝜑 → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
648, 5atbase 36547 . . . . . . . 8 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
6514, 64syl 17 . . . . . . 7 (𝜑𝑃 ∈ (Base‘𝐾))
668, 5atbase 36547 . . . . . . . 8 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
6715, 66syl 17 . . . . . . 7 (𝜑𝑆 ∈ (Base‘𝐾))
688, 4latj32 17698 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑃 𝑄) 𝑆) = ((𝑃 𝑆) 𝑄))
693, 65, 38, 67, 68syl13anc 1369 . . . . . 6 (𝜑 → ((𝑃 𝑄) 𝑆) = ((𝑃 𝑆) 𝑄))
708, 4latjjdi 17704 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (𝑃 (𝑄 𝑆)) = ((𝑃 𝑄) (𝑃 𝑆)))
713, 65, 38, 67, 70syl13anc 1369 . . . . . 6 (𝜑 → (𝑃 (𝑄 𝑆)) = ((𝑃 𝑄) (𝑃 𝑆)))
7263, 69, 713eqtr3rd 2866 . . . . 5 (𝜑 → ((𝑃 𝑄) (𝑃 𝑆)) = ((𝑃 𝑆) 𝑄))
7361, 72breqtrd 5068 . . . 4 (𝜑 → (𝑈 𝑉) ((𝑃 𝑆) 𝑄))
748, 18, 3, 32, 36, 40, 45, 73lattrd 17659 . . 3 (𝜑𝑇 ((𝑃 𝑆) 𝑄))
7518, 4, 9, 52atmat 36819 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) ∧ (𝑄𝐴𝑇𝐴𝑃𝑆) ∧ (𝑄𝑇 ∧ ¬ 𝑄 (𝑃 𝑆) ∧ 𝑇 ((𝑃 𝑆) 𝑄))) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ 𝐴)
7613, 14, 15, 16, 17, 19, 26, 30, 74, 75syl333anc 1399 . 2 (𝜑 → ((𝑃 𝑆) (𝑄 𝑇)) ∈ 𝐴)
7712, 76eqeltrd 2914 1 (𝜑𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  wne 3011   class class class wbr 5042  cfv 6334  (class class class)co 7140  Basecbs 16474  lecple 16563  joincjn 17545  meetcmee 17546  Latclat 17646  Atomscatm 36521  CvLatclc 36523  HLchlt 36608  LHypclh 37242
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 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
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 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-proset 17529  df-poset 17547  df-plt 17559  df-lub 17575  df-glb 17576  df-join 17577  df-meet 17578  df-p0 17640  df-p1 17641  df-lat 17647  df-clat 17709  df-oposet 36434  df-ol 36436  df-oml 36437  df-covers 36524  df-ats 36525  df-atl 36556  df-cvlat 36580  df-hlat 36609  df-llines 36756  df-lplanes 36757  df-lhyp 37246
This theorem is referenced by:  4atexlemnclw  37328  4atexlemex2  37329  4atexlemcnd  37330
  Copyright terms: Public domain W3C validator