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

Theorem lvoli2 35362
Description: The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012.)
Hypotheses
Ref Expression
lvoli2.l = (le‘𝐾)
lvoli2.j = (join‘𝐾)
lvoli2.a 𝐴 = (Atoms‘𝐾)
lvoli2.v 𝑉 = (LVols‘𝐾)
Assertion
Ref Expression
lvoli2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉)

Proof of Theorem lvoli2
Dummy variables 𝑞 𝑝 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp12 1244 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑃𝐴)
2 simp13 1245 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑄𝐴)
3 simp3 1132 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)))
4 eqidd 2753 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑄) 𝑅) 𝑆))
5 neeq1 2986 . . . . . . . . 9 (𝑝 = 𝑃 → (𝑝𝑞𝑃𝑞))
6 oveq1 6812 . . . . . . . . . . 11 (𝑝 = 𝑃 → (𝑝 𝑞) = (𝑃 𝑞))
76breq2d 4808 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑅 (𝑝 𝑞) ↔ 𝑅 (𝑃 𝑞)))
87notbid 307 . . . . . . . . 9 (𝑝 = 𝑃 → (¬ 𝑅 (𝑝 𝑞) ↔ ¬ 𝑅 (𝑃 𝑞)))
96oveq1d 6820 . . . . . . . . . . 11 (𝑝 = 𝑃 → ((𝑝 𝑞) 𝑅) = ((𝑃 𝑞) 𝑅))
109breq2d 4808 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑆 ((𝑝 𝑞) 𝑅) ↔ 𝑆 ((𝑃 𝑞) 𝑅)))
1110notbid 307 . . . . . . . . 9 (𝑝 = 𝑃 → (¬ 𝑆 ((𝑝 𝑞) 𝑅) ↔ ¬ 𝑆 ((𝑃 𝑞) 𝑅)))
125, 8, 113anbi123d 1540 . . . . . . . 8 (𝑝 = 𝑃 → ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ↔ (𝑃𝑞 ∧ ¬ 𝑅 (𝑃 𝑞) ∧ ¬ 𝑆 ((𝑃 𝑞) 𝑅))))
139oveq1d 6820 . . . . . . . . 9 (𝑝 = 𝑃 → (((𝑝 𝑞) 𝑅) 𝑆) = (((𝑃 𝑞) 𝑅) 𝑆))
1413eqeq2d 2762 . . . . . . . 8 (𝑝 = 𝑃 → ((((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆) ↔ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑞) 𝑅) 𝑆)))
1512, 14anbi12d 749 . . . . . . 7 (𝑝 = 𝑃 → (((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)) ↔ ((𝑃𝑞 ∧ ¬ 𝑅 (𝑃 𝑞) ∧ ¬ 𝑆 ((𝑃 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑞) 𝑅) 𝑆))))
16 neeq2 2987 . . . . . . . . 9 (𝑞 = 𝑄 → (𝑃𝑞𝑃𝑄))
17 oveq2 6813 . . . . . . . . . . 11 (𝑞 = 𝑄 → (𝑃 𝑞) = (𝑃 𝑄))
1817breq2d 4808 . . . . . . . . . 10 (𝑞 = 𝑄 → (𝑅 (𝑃 𝑞) ↔ 𝑅 (𝑃 𝑄)))
1918notbid 307 . . . . . . . . 9 (𝑞 = 𝑄 → (¬ 𝑅 (𝑃 𝑞) ↔ ¬ 𝑅 (𝑃 𝑄)))
2017oveq1d 6820 . . . . . . . . . . 11 (𝑞 = 𝑄 → ((𝑃 𝑞) 𝑅) = ((𝑃 𝑄) 𝑅))
2120breq2d 4808 . . . . . . . . . 10 (𝑞 = 𝑄 → (𝑆 ((𝑃 𝑞) 𝑅) ↔ 𝑆 ((𝑃 𝑄) 𝑅)))
2221notbid 307 . . . . . . . . 9 (𝑞 = 𝑄 → (¬ 𝑆 ((𝑃 𝑞) 𝑅) ↔ ¬ 𝑆 ((𝑃 𝑄) 𝑅)))
2316, 19, 223anbi123d 1540 . . . . . . . 8 (𝑞 = 𝑄 → ((𝑃𝑞 ∧ ¬ 𝑅 (𝑃 𝑞) ∧ ¬ 𝑆 ((𝑃 𝑞) 𝑅)) ↔ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))))
2420oveq1d 6820 . . . . . . . . 9 (𝑞 = 𝑄 → (((𝑃 𝑞) 𝑅) 𝑆) = (((𝑃 𝑄) 𝑅) 𝑆))
2524eqeq2d 2762 . . . . . . . 8 (𝑞 = 𝑄 → ((((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑞) 𝑅) 𝑆) ↔ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑄) 𝑅) 𝑆)))
2623, 25anbi12d 749 . . . . . . 7 (𝑞 = 𝑄 → (((𝑃𝑞 ∧ ¬ 𝑅 (𝑃 𝑞) ∧ ¬ 𝑆 ((𝑃 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑞) 𝑅) 𝑆)) ↔ ((𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑄) 𝑅) 𝑆))))
2715, 26rspc2ev 3455 . . . . . 6 ((𝑃𝐴𝑄𝐴 ∧ ((𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑃 𝑄) 𝑅) 𝑆))) → ∃𝑝𝐴𝑞𝐴 ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)))
281, 2, 3, 4, 27syl112anc 1477 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ∃𝑝𝐴𝑞𝐴 ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)))
29283exp 1112 . . . 4 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → ((𝑅𝐴𝑆𝐴) → ((𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → ∃𝑝𝐴𝑞𝐴 ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)))))
30 simplrl 819 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆))) → 𝑅𝐴)
31 simplrr 820 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆))) → 𝑆𝐴)
32 simpr 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆))) → ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)))
33 breq1 4799 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → (𝑟 (𝑝 𝑞) ↔ 𝑅 (𝑝 𝑞)))
3433notbid 307 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (¬ 𝑟 (𝑝 𝑞) ↔ ¬ 𝑅 (𝑝 𝑞)))
35 oveq2 6813 . . . . . . . . . . . . . 14 (𝑟 = 𝑅 → ((𝑝 𝑞) 𝑟) = ((𝑝 𝑞) 𝑅))
3635breq2d 4808 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → (𝑠 ((𝑝 𝑞) 𝑟) ↔ 𝑠 ((𝑝 𝑞) 𝑅)))
3736notbid 307 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (¬ 𝑠 ((𝑝 𝑞) 𝑟) ↔ ¬ 𝑠 ((𝑝 𝑞) 𝑅)))
3834, 373anbi23d 1543 . . . . . . . . . . 11 (𝑟 = 𝑅 → ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ↔ (𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑅))))
3935oveq1d 6820 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (((𝑝 𝑞) 𝑟) 𝑠) = (((𝑝 𝑞) 𝑅) 𝑠))
4039eqeq2d 2762 . . . . . . . . . . 11 (𝑟 = 𝑅 → ((((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠) ↔ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑠)))
4138, 40anbi12d 749 . . . . . . . . . 10 (𝑟 = 𝑅 → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑠))))
42 breq1 4799 . . . . . . . . . . . . 13 (𝑠 = 𝑆 → (𝑠 ((𝑝 𝑞) 𝑅) ↔ 𝑆 ((𝑝 𝑞) 𝑅)))
4342notbid 307 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (¬ 𝑠 ((𝑝 𝑞) 𝑅) ↔ ¬ 𝑆 ((𝑝 𝑞) 𝑅)))
44433anbi3d 1546 . . . . . . . . . . 11 (𝑠 = 𝑆 → ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑅)) ↔ (𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅))))
45 oveq2 6813 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (((𝑝 𝑞) 𝑅) 𝑠) = (((𝑝 𝑞) 𝑅) 𝑆))
4645eqeq2d 2762 . . . . . . . . . . 11 (𝑠 = 𝑆 → ((((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑠) ↔ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)))
4744, 46anbi12d 749 . . . . . . . . . 10 (𝑠 = 𝑆 → (((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑠)) ↔ ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆))))
4841, 47rspc2ev 3455 . . . . . . . . 9 ((𝑅𝐴𝑆𝐴 ∧ ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆))) → ∃𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠)))
4930, 31, 32, 48syl3anc 1473 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) ∧ ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆))) → ∃𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠)))
5049ex 449 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)) → ∃𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠))))
5150reximdv 3146 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (∃𝑞𝐴 ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠))))
5251reximdv 3146 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴)) → (∃𝑝𝐴𝑞𝐴 ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)) → ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠))))
5352ex 449 . . . 4 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → ((𝑅𝐴𝑆𝐴) → (∃𝑝𝐴𝑞𝐴 ((𝑝𝑞 ∧ ¬ 𝑅 (𝑝 𝑞) ∧ ¬ 𝑆 ((𝑝 𝑞) 𝑅)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑅) 𝑆)) → ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠)))))
5429, 53syldd 72 . . 3 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → ((𝑅𝐴𝑆𝐴) → ((𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅)) → ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠)))))
55543imp 1101 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠)))
56 simp11 1243 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝐾 ∈ HL)
57 hllat 35145 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ Lat)
5856, 57syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝐾 ∈ Lat)
59 eqid 2752 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
60 lvoli2.j . . . . . . 7 = (join‘𝐾)
61 lvoli2.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
6259, 60, 61hlatjcl 35148 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
63623ad2ant1 1127 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (𝑃 𝑄) ∈ (Base‘𝐾))
64 simp2l 1239 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑅𝐴)
6559, 61atbase 35071 . . . . . 6 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
6664, 65syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑅 ∈ (Base‘𝐾))
6759, 60latjcl 17244 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
6858, 63, 66, 67syl3anc 1473 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
69 simp2r 1240 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑆𝐴)
7059, 61atbase 35071 . . . . 5 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
7169, 70syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → 𝑆 ∈ (Base‘𝐾))
7259, 60latjcl 17244 . . . 4 ((𝐾 ∈ Lat ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ (Base‘𝐾))
7358, 68, 71, 72syl3anc 1473 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ (Base‘𝐾))
74 lvoli2.l . . . 4 = (le‘𝐾)
75 lvoli2.v . . . 4 𝑉 = (LVols‘𝐾)
7659, 74, 60, 61, 75islvol5 35360 . . 3 ((𝐾 ∈ HL ∧ (((𝑃 𝑄) 𝑅) 𝑆) ∈ (Base‘𝐾)) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠))))
7756, 73, 76syl2anc 696 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → ((((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉 ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ (((𝑃 𝑄) 𝑅) 𝑆) = (((𝑝 𝑞) 𝑟) 𝑠))))
7855, 77mpbird 247 1 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 ((𝑃 𝑄) 𝑅))) → (((𝑃 𝑄) 𝑅) 𝑆) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1624  wcel 2131  wne 2924  wrex 3043   class class class wbr 4796  cfv 6041  (class class class)co 6805  Basecbs 16051  lecple 16142  joincjn 17137  Latclat 17238  Atomscatm 35045  HLchlt 35132  LVolsclvol 35274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-reu 3049  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-preset 17121  df-poset 17139  df-plt 17151  df-lub 17167  df-glb 17168  df-join 17169  df-meet 17170  df-p0 17232  df-lat 17239  df-clat 17301  df-oposet 34958  df-ol 34960  df-oml 34961  df-covers 35048  df-ats 35049  df-atl 35080  df-cvlat 35104  df-hlat 35133  df-llines 35279  df-lplanes 35280  df-lvols 35281
This theorem is referenced by:  islvol2aN  35373  4atlem3  35377  2lplnja  35400
  Copyright terms: Public domain W3C validator