Metamath Proof Explorer

Theorem islvol3

Description: The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012)

Ref Expression
Hypotheses islvol3.b ⊢ B = Base K
islvol3.l ⊢ ≤ ˙ = ≤ K
islvol3.j ⊢ ∨ ˙ = join ⁡ K
islvol3.a ⊢ A = Atoms ⁡ K
islvol3.p ⊢ P = LPlanes ⁡ K
islvol3.v ⊢ V = LVols ⁡ K
Assertion islvol3 ⊢ K ∈ HL ∧ X ∈ B → X ∈ V ↔ ∃ y ∈ P ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p

Proof

Step Hyp Ref Expression
1 islvol3.b ⊢ B = Base K
2 islvol3.l ⊢ ≤ ˙ = ≤ K
3 islvol3.j ⊢ ∨ ˙ = join ⁡ K
4 islvol3.a ⊢ A = Atoms ⁡ K
5 islvol3.p ⊢ P = LPlanes ⁡ K
6 islvol3.v ⊢ V = LVols ⁡ K
7 eqid ⊢ ⋖ K = ⋖ K
8 1 7 5 6 islvol4 ⊢ K ∈ HL ∧ X ∈ B → X ∈ V ↔ ∃ y ∈ P y ⋖ K X
9 simpll ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P → K ∈ HL
10 1 5 lplnbase ⊢ y ∈ P → y ∈ B
11 10 adantl ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P → y ∈ B
12 simplr ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P → X ∈ B
13 1 2 3 7 4 cvrval3 ⊢ K ∈ HL ∧ y ∈ B ∧ X ∈ B → y ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X
14 9 11 12 13 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P → y ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X
15 eqcom ⊢ y ∨ ˙ p = X ↔ X = y ∨ ˙ p
16 15 a1i ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P ∧ p ∈ A → y ∨ ˙ p = X ↔ X = y ∨ ˙ p
17 16 anbi2d ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P ∧ p ∈ A → ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X ↔ ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
18 17 rexbidva ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P → ∃ p ∈ A ¬ p ≤ ˙ y ∧ y ∨ ˙ p = X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
19 14 18 bitrd ⊢ K ∈ HL ∧ X ∈ B ∧ y ∈ P → y ⋖ K X ↔ ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
20 19 rexbidva ⊢ K ∈ HL ∧ X ∈ B → ∃ y ∈ P y ⋖ K X ↔ ∃ y ∈ P ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p
21 8 20 bitrd ⊢ K ∈ HL ∧ X ∈ B → X ∈ V ↔ ∃ y ∈ P ∃ p ∈ A ¬ p ≤ ˙ y ∧ X = y ∨ ˙ p