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

Theorem 4atexlemcnd 36142
Description: Lemma for 4atexlem7 36145. (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 𝐶 = ((𝑄 𝑇) (𝑃 𝑆))
4thatlem0.d 𝐷 = ((𝑅 𝑇) (𝑃 𝑆))
Assertion
Ref Expression
4atexlemcnd (𝜑𝐶𝐷)

Proof of Theorem 4atexlemcnd
StepHypRef Expression
1 4thatlem.ph . . . 4 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑆𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ (𝑃 𝑅) = (𝑄 𝑅)) ∧ (𝑇𝐴 ∧ (𝑈 𝑇) = (𝑉 𝑇))) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))))
2 4thatlem0.l . . . 4 = (le‘𝐾)
3 4thatlem0.j . . . 4 = (join‘𝐾)
4 4thatlem0.m . . . 4 = (meet‘𝐾)
5 4thatlem0.a . . . 4 𝐴 = (Atoms‘𝐾)
6 4thatlem0.h . . . 4 𝐻 = (LHyp‘𝐾)
7 4thatlem0.u . . . 4 𝑈 = ((𝑃 𝑄) 𝑊)
8 4thatlem0.v . . . 4 𝑉 = ((𝑃 𝑆) 𝑊)
91, 2, 3, 4, 5, 6, 7, 84atexlemtlw 36137 . . 3 (𝜑𝑇 𝑊)
10 4thatlem0.c . . . 4 𝐶 = ((𝑄 𝑇) (𝑃 𝑆))
111, 2, 3, 4, 5, 6, 7, 8, 104atexlemnclw 36140 . . 3 (𝜑 → ¬ 𝐶 𝑊)
12 nbrne2 4895 . . 3 ((𝑇 𝑊 ∧ ¬ 𝐶 𝑊) → 𝑇𝐶)
139, 11, 12syl2anc 579 . 2 (𝜑𝑇𝐶)
1414atexlemk 36117 . . . . . . . . 9 (𝜑𝐾 ∈ HL)
1514atexlemq 36121 . . . . . . . . 9 (𝜑𝑄𝐴)
1614atexlemt 36123 . . . . . . . . 9 (𝜑𝑇𝐴)
173, 5hlatjcom 35438 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴) → (𝑄 𝑇) = (𝑇 𝑄))
1814, 15, 16, 17syl3anc 1494 . . . . . . . 8 (𝜑 → (𝑄 𝑇) = (𝑇 𝑄))
19 simp221 1417 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑆𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ (𝑃 𝑅) = (𝑄 𝑅)) ∧ (𝑇𝐴 ∧ (𝑈 𝑇) = (𝑉 𝑇))) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅𝐴)
201, 19sylbi 209 . . . . . . . . 9 (𝜑𝑅𝐴)
213, 5hlatjcom 35438 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑇𝐴) → (𝑅 𝑇) = (𝑇 𝑅))
2214, 20, 16, 21syl3anc 1494 . . . . . . . 8 (𝜑 → (𝑅 𝑇) = (𝑇 𝑅))
2318, 22oveq12d 6928 . . . . . . 7 (𝜑 → ((𝑄 𝑇) (𝑅 𝑇)) = ((𝑇 𝑄) (𝑇 𝑅)))
2414atexlemkc 36128 . . . . . . . . 9 (𝜑𝐾 ∈ CvLat)
2514atexlemp 36120 . . . . . . . . 9 (𝜑𝑃𝐴)
2614atexlempnq 36125 . . . . . . . . 9 (𝜑𝑃𝑄)
27 simp223 1419 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑆𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ (𝑃 𝑅) = (𝑄 𝑅)) ∧ (𝑇𝐴 ∧ (𝑈 𝑇) = (𝑉 𝑇))) ∧ (𝑃𝑄 ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑃 𝑅) = (𝑄 𝑅))
281, 27sylbi 209 . . . . . . . . 9 (𝜑 → (𝑃 𝑅) = (𝑄 𝑅))
295, 3cvlsupr6 35417 . . . . . . . . . 10 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ (𝑃 𝑅) = (𝑄 𝑅))) → 𝑅𝑄)
3029necomd 3054 . . . . . . . . 9 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ (𝑃 𝑅) = (𝑄 𝑅))) → 𝑄𝑅)
3124, 25, 15, 20, 26, 28, 30syl132anc 1511 . . . . . . . 8 (𝜑𝑄𝑅)
321, 2, 3, 4, 5, 6, 7, 84atexlemntlpq 36138 . . . . . . . . 9 (𝜑 → ¬ 𝑇 (𝑃 𝑄))
335, 3cvlsupr7 35418 . . . . . . . . . . . 12 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ (𝑃 𝑅) = (𝑄 𝑅))) → (𝑃 𝑄) = (𝑅 𝑄))
3424, 25, 15, 20, 26, 28, 33syl132anc 1511 . . . . . . . . . . 11 (𝜑 → (𝑃 𝑄) = (𝑅 𝑄))
353, 5hlatjcom 35438 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) = (𝑅 𝑄))
3614, 15, 20, 35syl3anc 1494 . . . . . . . . . . 11 (𝜑 → (𝑄 𝑅) = (𝑅 𝑄))
3734, 36eqtr4d 2864 . . . . . . . . . 10 (𝜑 → (𝑃 𝑄) = (𝑄 𝑅))
3837breq2d 4887 . . . . . . . . 9 (𝜑 → (𝑇 (𝑃 𝑄) ↔ 𝑇 (𝑄 𝑅)))
3932, 38mtbid 316 . . . . . . . 8 (𝜑 → ¬ 𝑇 (𝑄 𝑅))
402, 3, 4, 52llnma2 35859 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑅𝐴𝑇𝐴) ∧ (𝑄𝑅 ∧ ¬ 𝑇 (𝑄 𝑅))) → ((𝑇 𝑄) (𝑇 𝑅)) = 𝑇)
4114, 15, 20, 16, 31, 39, 40syl132anc 1511 . . . . . . 7 (𝜑 → ((𝑇 𝑄) (𝑇 𝑅)) = 𝑇)
4223, 41eqtr2d 2862 . . . . . 6 (𝜑𝑇 = ((𝑄 𝑇) (𝑅 𝑇)))
4342adantr 474 . . . . 5 ((𝜑𝐶 = 𝐷) → 𝑇 = ((𝑄 𝑇) (𝑅 𝑇)))
4414atexlemkl 36127 . . . . . . . . . 10 (𝜑𝐾 ∈ Lat)
451, 3, 54atexlemqtb 36131 . . . . . . . . . 10 (𝜑 → (𝑄 𝑇) ∈ (Base‘𝐾))
461, 3, 54atexlempsb 36130 . . . . . . . . . 10 (𝜑 → (𝑃 𝑆) ∈ (Base‘𝐾))
47 eqid 2825 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
4847, 2, 4latmle1 17436 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑄 𝑇) (𝑃 𝑆)) (𝑄 𝑇))
4944, 45, 46, 48syl3anc 1494 . . . . . . . . 9 (𝜑 → ((𝑄 𝑇) (𝑃 𝑆)) (𝑄 𝑇))
5010, 49syl5eqbr 4910 . . . . . . . 8 (𝜑𝐶 (𝑄 𝑇))
5150adantr 474 . . . . . . 7 ((𝜑𝐶 = 𝐷) → 𝐶 (𝑄 𝑇))
52 simpr 479 . . . . . . . 8 ((𝜑𝐶 = 𝐷) → 𝐶 = 𝐷)
53 4thatlem0.d . . . . . . . . . 10 𝐷 = ((𝑅 𝑇) (𝑃 𝑆))
5447, 3, 5hlatjcl 35437 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑇𝐴) → (𝑅 𝑇) ∈ (Base‘𝐾))
5514, 20, 16, 54syl3anc 1494 . . . . . . . . . . 11 (𝜑 → (𝑅 𝑇) ∈ (Base‘𝐾))
5647, 2, 4latmle1 17436 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑅 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑇) (𝑃 𝑆)) (𝑅 𝑇))
5744, 55, 46, 56syl3anc 1494 . . . . . . . . . 10 (𝜑 → ((𝑅 𝑇) (𝑃 𝑆)) (𝑅 𝑇))
5853, 57syl5eqbr 4910 . . . . . . . . 9 (𝜑𝐷 (𝑅 𝑇))
5958adantr 474 . . . . . . . 8 ((𝜑𝐶 = 𝐷) → 𝐷 (𝑅 𝑇))
6052, 59eqbrtrd 4897 . . . . . . 7 ((𝜑𝐶 = 𝐷) → 𝐶 (𝑅 𝑇))
611, 2, 3, 4, 5, 6, 7, 8, 104atexlemc 36139 . . . . . . . . . 10 (𝜑𝐶𝐴)
6247, 5atbase 35359 . . . . . . . . . 10 (𝐶𝐴𝐶 ∈ (Base‘𝐾))
6361, 62syl 17 . . . . . . . . 9 (𝜑𝐶 ∈ (Base‘𝐾))
6447, 2, 4latlem12 17438 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ (𝑄 𝑇) ∈ (Base‘𝐾) ∧ (𝑅 𝑇) ∈ (Base‘𝐾))) → ((𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑇)) ↔ 𝐶 ((𝑄 𝑇) (𝑅 𝑇))))
6544, 63, 45, 55, 64syl13anc 1495 . . . . . . . 8 (𝜑 → ((𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑇)) ↔ 𝐶 ((𝑄 𝑇) (𝑅 𝑇))))
6665adantr 474 . . . . . . 7 ((𝜑𝐶 = 𝐷) → ((𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑇)) ↔ 𝐶 ((𝑄 𝑇) (𝑅 𝑇))))
6751, 60, 66mpbi2and 703 . . . . . 6 ((𝜑𝐶 = 𝐷) → 𝐶 ((𝑄 𝑇) (𝑅 𝑇)))
68 hlatl 35430 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
6914, 68syl 17 . . . . . . . 8 (𝜑𝐾 ∈ AtLat)
7042, 16eqeltrrd 2907 . . . . . . . 8 (𝜑 → ((𝑄 𝑇) (𝑅 𝑇)) ∈ 𝐴)
712, 5atcmp 35381 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝐶𝐴 ∧ ((𝑄 𝑇) (𝑅 𝑇)) ∈ 𝐴) → (𝐶 ((𝑄 𝑇) (𝑅 𝑇)) ↔ 𝐶 = ((𝑄 𝑇) (𝑅 𝑇))))
7269, 61, 70, 71syl3anc 1494 . . . . . . 7 (𝜑 → (𝐶 ((𝑄 𝑇) (𝑅 𝑇)) ↔ 𝐶 = ((𝑄 𝑇) (𝑅 𝑇))))
7372adantr 474 . . . . . 6 ((𝜑𝐶 = 𝐷) → (𝐶 ((𝑄 𝑇) (𝑅 𝑇)) ↔ 𝐶 = ((𝑄 𝑇) (𝑅 𝑇))))
7467, 73mpbid 224 . . . . 5 ((𝜑𝐶 = 𝐷) → 𝐶 = ((𝑄 𝑇) (𝑅 𝑇)))
7543, 74eqtr4d 2864 . . . 4 ((𝜑𝐶 = 𝐷) → 𝑇 = 𝐶)
7675ex 403 . . 3 (𝜑 → (𝐶 = 𝐷𝑇 = 𝐶))
7776necon3d 3020 . 2 (𝜑 → (𝑇𝐶𝐶𝐷))
7813, 77mpd 15 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1111   = wceq 1656  wcel 2164  wne 2999   class class class wbr 4875  cfv 6127  (class class class)co 6910  Basecbs 16229  lecple 16319  joincjn 17304  meetcmee 17305  Latclat 17405  Atomscatm 35333  AtLatcal 35334  CvLatclc 35335  HLchlt 35420  LHypclh 36054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-riota 6871  df-ov 6913  df-oprab 6914  df-proset 17288  df-poset 17306  df-plt 17318  df-lub 17334  df-glb 17335  df-join 17336  df-meet 17337  df-p0 17399  df-p1 17400  df-lat 17406  df-clat 17468  df-oposet 35246  df-ol 35248  df-oml 35249  df-covers 35336  df-ats 35337  df-atl 35368  df-cvlat 35392  df-hlat 35421  df-llines 35568  df-lplanes 35569  df-lhyp 36058
This theorem is referenced by:  4atexlemex4  36143
  Copyright terms: Public domain W3C validator