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

Theorem islvol2aN 37600
Description: The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
islvol2a.l = (le‘𝐾)
islvol2a.j = (join‘𝐾)
islvol2a.a 𝐴 = (Atoms‘𝐾)
islvol2a.v 𝑉 = (LVols‘𝐾)
Assertion
Ref Expression
islvol2aN (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))))

Proof of Theorem islvol2aN
StepHypRef Expression
1 oveq1 7276 . . . . . . . . 9 (𝑃 = 𝑄 → (𝑃 𝑄) = (𝑄 𝑄))
2 simpl1 1190 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝐾 ∈ HL)
3 simpl3 1192 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝑄𝐴)
4 islvol2a.j . . . . . . . . . . 11 = (join‘𝐾)
5 islvol2a.a . . . . . . . . . . 11 𝐴 = (Atoms‘𝐾)
64, 5hlatjidm 37377 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑄𝐴) → (𝑄 𝑄) = 𝑄)
72, 3, 6syl2anc 584 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (𝑄 𝑄) = 𝑄)
81, 7sylan9eqr 2802 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃 = 𝑄) → (𝑃 𝑄) = 𝑄)
98oveq1d 7284 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃 = 𝑄) → ((𝑃 𝑄) 𝑅) = (𝑄 𝑅))
109oveq1d 7284 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃 = 𝑄) → (((𝑃 𝑄) 𝑅) 𝑆) = ((𝑄 𝑅) 𝑆))
11 simprl 768 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝑅𝐴)
12 simprr 770 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝑆𝐴)
13 islvol2a.v . . . . . . . . 9 𝑉 = (LVols‘𝐾)
144, 5, 133atnelvolN 37594 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑅𝐴𝑆𝐴)) → ¬ ((𝑄 𝑅) 𝑆) ∈ 𝑉)
152, 3, 11, 12, 14syl13anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ¬ ((𝑄 𝑅) 𝑆) ∈ 𝑉)
1615adantr 481 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃 = 𝑄) → ¬ ((𝑄 𝑅) 𝑆) ∈ 𝑉)
1710, 16eqneltrd 2860 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃 = 𝑄) → ¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉)
1817ex 413 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (𝑃 = 𝑄 → ¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉))
1918necon2ad 2960 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉𝑃𝑄))
202hllatd 37372 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝐾 ∈ Lat)
21 eqid 2740 . . . . . . . 8 (Base‘𝐾) = (Base‘𝐾)
2221, 5atbase 37297 . . . . . . 7 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
2322ad2antrl 725 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝑅 ∈ (Base‘𝐾))
2421, 4, 5hlatjcl 37375 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
2524adantr 481 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
26 islvol2a.l . . . . . . 7 = (le‘𝐾)
2721, 26, 4latleeqj2 18166 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
2820, 23, 25, 27syl3anc 1370 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
29 simpl2 1191 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝑃𝐴)
304, 5, 133atnelvolN 37594 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → ¬ ((𝑃 𝑄) 𝑆) ∈ 𝑉)
312, 29, 3, 12, 30syl13anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ¬ ((𝑃 𝑄) 𝑆) ∈ 𝑉)
32 oveq1 7276 . . . . . . . 8 (((𝑃 𝑄) 𝑅) = (𝑃 𝑄) → (((𝑃 𝑄) 𝑅) 𝑆) = ((𝑃 𝑄) 𝑆))
3332eleq1d 2825 . . . . . . 7 (((𝑃 𝑄) 𝑅) = (𝑃 𝑄) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ ((𝑃 𝑄) 𝑆) ∈ 𝑉))
3433notbid 318 . . . . . 6 (((𝑃 𝑄) 𝑅) = (𝑃 𝑄) → (¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ ¬ ((𝑃 𝑄) 𝑆) ∈ 𝑉))
3531, 34syl5ibrcom 246 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (((𝑃 𝑄) 𝑅) = (𝑃 𝑄) → ¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉))
3628, 35sylbid 239 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (𝑅 (𝑃 𝑄) → ¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉))
3736con2d 134 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 → ¬ 𝑅 (𝑃 𝑄)))
3821, 5atbase 37297 . . . . . . 7 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
3938ad2antll 726 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → 𝑆 ∈ (Base‘𝐾))
4021, 4latjcl 18153 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
4120, 25, 23, 40syl3anc 1370 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
4221, 26, 4latleeqj2 18166 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾)) → (𝑆 ((𝑃 𝑄) 𝑅) ↔ (((𝑃 𝑄) 𝑅) 𝑆) = ((𝑃 𝑄) 𝑅)))
4320, 39, 41, 42syl3anc 1370 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (𝑆 ((𝑃 𝑄) 𝑅) ↔ (((𝑃 𝑄) 𝑅) 𝑆) = ((𝑃 𝑄) 𝑅)))
444, 5, 133atnelvolN 37594 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ¬ ((𝑃 𝑄) 𝑅) ∈ 𝑉)
452, 29, 3, 11, 44syl13anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ¬ ((𝑃 𝑄) 𝑅) ∈ 𝑉)
46 eleq1 2828 . . . . . . 7 ((((𝑃 𝑄) 𝑅) 𝑆) = ((𝑃 𝑄) 𝑅) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ ((𝑃 𝑄) 𝑅) ∈ 𝑉))
4746notbid 318 . . . . . 6 ((((𝑃 𝑄) 𝑅) 𝑆) = ((𝑃 𝑄) 𝑅) → (¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ ¬ ((𝑃 𝑄) 𝑅) ∈ 𝑉))
4845, 47syl5ibrcom 246 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((((𝑃 𝑄) 𝑅) 𝑆) = ((𝑃 𝑄) 𝑅) → ¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉))
4943, 48sylbid 239 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (𝑆 ((𝑃 𝑄) 𝑅) → ¬ (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉))
5049con2d 134 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 → ¬ 𝑆 ((𝑃 𝑄) 𝑅)))
5119, 37, 503jcad 1128 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))))
5226, 4, 5, 13lvoli2 37589 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉)
53523expia 1120 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉))
5451, 53impbid 211 1 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wcel 2110  wne 2945   class class class wbr 5079  cfv 6431  (class class class)co 7269  Basecbs 16908  lecple 16965  joincjn 18025  Latclat 18145  Atomscatm 37271  HLchlt 37358  LVolsclvol 37501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-proset 18009  df-poset 18027  df-plt 18044  df-lub 18060  df-glb 18061  df-join 18062  df-meet 18063  df-p0 18139  df-lat 18146  df-clat 18213  df-oposet 37184  df-ol 37186  df-oml 37187  df-covers 37274  df-ats 37275  df-atl 37306  df-cvlat 37330  df-hlat 37359  df-llines 37506  df-lplanes 37507  df-lvols 37508
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator