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 38521
Description: Lemma for 4atexlem7 38527. (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 38509 . . . 4 (𝜑𝐾 ∈ Lat)
4 4thatlem0.j . . . . 5 = (join‘𝐾)
5 4thatlem0.a . . . . 5 𝐴 = (Atoms‘𝐾)
62, 4, 54atexlemqtb 38513 . . . 4 (𝜑 → (𝑄 𝑇) ∈ (Base‘𝐾))
72, 4, 54atexlempsb 38512 . . . 4 (𝜑 → (𝑃 𝑆) ∈ (Base‘𝐾))
8 eqid 2736 . . . . 5 (Base‘𝐾) = (Base‘𝐾)
9 4thatlem0.m . . . . 5 = (meet‘𝐾)
108, 9latmcom 18349 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
113, 6, 7, 10syl3anc 1371 . . 3 (𝜑 → ((𝑄 𝑇) (𝑃 𝑆)) = ((𝑃 𝑆) (𝑄 𝑇)))
121, 11eqtrid 2788 . 2 (𝜑𝐶 = ((𝑃 𝑆) (𝑄 𝑇)))
1324atexlemk 38499 . . 3 (𝜑𝐾 ∈ HL)
1424atexlemp 38502 . . 3 (𝜑𝑃𝐴)
1524atexlems 38504 . . 3 (𝜑𝑆𝐴)
1624atexlemq 38503 . . 3 (𝜑𝑄𝐴)
1724atexlemt 38505 . . 3 (𝜑𝑇𝐴)
18 4thatlem0.l . . . 4 = (le‘𝐾)
192, 18, 4, 54atexlempns 38514 . . 3 (𝜑𝑃𝑆)
20 4thatlem0.h . . . . 5 𝐻 = (LHyp‘𝐾)
21 4thatlem0.u . . . . 5 𝑈 = ((𝑃 𝑄) 𝑊)
22 4thatlem0.v . . . . 5 𝑉 = ((𝑃 𝑆) 𝑊)
232, 18, 4, 9, 5, 20, 21, 224atexlemntlpq 38520 . . . 4 (𝜑 → ¬ 𝑇 (𝑃 𝑄))
2418, 4, 5atnlej2 37832 . . . . 5 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑃𝐴𝑄𝐴) ∧ ¬ 𝑇 (𝑃 𝑄)) → 𝑇𝑄)
2524necomd 2998 . . . 4 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑃𝐴𝑄𝐴) ∧ ¬ 𝑇 (𝑃 𝑄)) → 𝑄𝑇)
2613, 17, 14, 16, 23, 25syl131anc 1383 . . 3 (𝜑𝑄𝑇)
2724atexlempnq 38507 . . . 4 (𝜑𝑃𝑄)
2824atexlemnslpq 38508 . . . 4 (𝜑 → ¬ 𝑆 (𝑃 𝑄))
2918, 4, 54atlem0ae 38046 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))) → ¬ 𝑄 (𝑃 𝑆))
3013, 14, 16, 15, 27, 28, 29syl132anc 1388 . . 3 (𝜑 → ¬ 𝑄 (𝑃 𝑆))
318, 5atbase 37740 . . . . 5 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
3217, 31syl 17 . . . 4 (𝜑𝑇 ∈ (Base‘𝐾))
332, 18, 4, 9, 5, 20, 214atexlemu 38516 . . . . 5 (𝜑𝑈𝐴)
342, 18, 4, 9, 5, 20, 21, 224atexlemv 38517 . . . . 5 (𝜑𝑉𝐴)
358, 4, 5hlatjcl 37818 . . . . 5 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴) → (𝑈 𝑉) ∈ (Base‘𝐾))
3613, 33, 34, 35syl3anc 1371 . . . 4 (𝜑 → (𝑈 𝑉) ∈ (Base‘𝐾))
378, 5atbase 37740 . . . . . 6 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
3816, 37syl 17 . . . . 5 (𝜑𝑄 ∈ (Base‘𝐾))
398, 4latjcl 18325 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
403, 7, 38, 39syl3anc 1371 . . . 4 (𝜑 → ((𝑃 𝑆) 𝑄) ∈ (Base‘𝐾))
4124atexlemkc 38510 . . . . 5 (𝜑𝐾 ∈ CvLat)
422, 18, 4, 9, 5, 20, 21, 224atexlemunv 38518 . . . . 5 (𝜑𝑈𝑉)
4324atexlemutvt 38506 . . . . 5 (𝜑 → (𝑈 𝑇) = (𝑉 𝑇))
445, 18, 4cvlsupr4 37796 . . . . 5 ((𝐾 ∈ CvLat ∧ (𝑈𝐴𝑉𝐴𝑇𝐴) ∧ (𝑈𝑉 ∧ (𝑈 𝑇) = (𝑉 𝑇))) → 𝑇 (𝑈 𝑉))
4541, 33, 34, 17, 42, 43, 44syl132anc 1388 . . . 4 (𝜑𝑇 (𝑈 𝑉))
468, 4, 5hlatjcl 37818 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
4713, 14, 16, 46syl3anc 1371 . . . . . . . 8 (𝜑 → (𝑃 𝑄) ∈ (Base‘𝐾))
482, 204atexlemwb 38511 . . . . . . . 8 (𝜑𝑊 ∈ (Base‘𝐾))
498, 18, 9latmle1 18350 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑊) (𝑃 𝑄))
503, 47, 48, 49syl3anc 1371 . . . . . . 7 (𝜑 → ((𝑃 𝑄) 𝑊) (𝑃 𝑄))
5121, 50eqbrtrid 5139 . . . . . 6 (𝜑𝑈 (𝑃 𝑄))
528, 18, 9latmle1 18350 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑊) (𝑃 𝑆))
533, 7, 48, 52syl3anc 1371 . . . . . . 7 (𝜑 → ((𝑃 𝑆) 𝑊) (𝑃 𝑆))
5422, 53eqbrtrid 5139 . . . . . 6 (𝜑𝑉 (𝑃 𝑆))
558, 5atbase 37740 . . . . . . . 8 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
5633, 55syl 17 . . . . . . 7 (𝜑𝑈 ∈ (Base‘𝐾))
578, 5atbase 37740 . . . . . . . 8 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
5834, 57syl 17 . . . . . . 7 (𝜑𝑉 ∈ (Base‘𝐾))
598, 18, 4latjlej12 18341 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) ∧ (𝑉 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾))) → ((𝑈 (𝑃 𝑄) ∧ 𝑉 (𝑃 𝑆)) → (𝑈 𝑉) ((𝑃 𝑄) (𝑃 𝑆))))
603, 56, 47, 58, 7, 59syl122anc 1379 . . . . . 6 (𝜑 → ((𝑈 (𝑃 𝑄) ∧ 𝑉 (𝑃 𝑆)) → (𝑈 𝑉) ((𝑃 𝑄) (𝑃 𝑆))))
6151, 54, 60mp2and 697 . . . . 5 (𝜑 → (𝑈 𝑉) ((𝑃 𝑄) (𝑃 𝑆)))
624, 5hlatjass 37821 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
6313, 14, 16, 15, 62syl13anc 1372 . . . . . 6 (𝜑 → ((𝑃 𝑄) 𝑆) = (𝑃 (𝑄 𝑆)))
648, 5atbase 37740 . . . . . . . 8 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
6514, 64syl 17 . . . . . . 7 (𝜑𝑃 ∈ (Base‘𝐾))
668, 5atbase 37740 . . . . . . . 8 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
6715, 66syl 17 . . . . . . 7 (𝜑𝑆 ∈ (Base‘𝐾))
688, 4latj32 18371 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → ((𝑃 𝑄) 𝑆) = ((𝑃 𝑆) 𝑄))
693, 65, 38, 67, 68syl13anc 1372 . . . . . 6 (𝜑 → ((𝑃 𝑄) 𝑆) = ((𝑃 𝑆) 𝑄))
708, 4latjjdi 18377 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (𝑃 (𝑄 𝑆)) = ((𝑃 𝑄) (𝑃 𝑆)))
713, 65, 38, 67, 70syl13anc 1372 . . . . . 6 (𝜑 → (𝑃 (𝑄 𝑆)) = ((𝑃 𝑄) (𝑃 𝑆)))
7263, 69, 713eqtr3rd 2785 . . . . 5 (𝜑 → ((𝑃 𝑄) (𝑃 𝑆)) = ((𝑃 𝑆) 𝑄))
7361, 72breqtrd 5130 . . . 4 (𝜑 → (𝑈 𝑉) ((𝑃 𝑆) 𝑄))
748, 18, 3, 32, 36, 40, 45, 73lattrd 18332 . . 3 (𝜑𝑇 ((𝑃 𝑆) 𝑄))
7518, 4, 9, 52atmat 38013 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) ∧ (𝑄𝐴𝑇𝐴𝑃𝑆) ∧ (𝑄𝑇 ∧ ¬ 𝑄 (𝑃 𝑆) ∧ 𝑇 ((𝑃 𝑆) 𝑄))) → ((𝑃 𝑆) (𝑄 𝑇)) ∈ 𝐴)
7613, 14, 15, 16, 17, 19, 26, 30, 74, 75syl333anc 1402 . 2 (𝜑 → ((𝑃 𝑆) (𝑄 𝑇)) ∈ 𝐴)
7712, 76eqeltrd 2838 1 (𝜑𝐶𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2942   class class class wbr 5104  cfv 6494  (class class class)co 7354  Basecbs 17080  lecple 17137  joincjn 18197  meetcmee 18198  Latclat 18317  Atomscatm 37714  CvLatclc 37716  HLchlt 37801  LHypclh 38436
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-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-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-llines 37950  df-lplanes 37951  df-lhyp 38440
This theorem is referenced by:  4atexlemnclw  38522  4atexlemex2  38523  4atexlemcnd  38524
  Copyright terms: Public domain W3C validator