Metamath Proof Explorer


Theorem islvol2

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

Ref Expression
Hypotheses islvol5.b B = Base K
islvol5.l ˙ = K
islvol5.j ˙ = join K
islvol5.a A = Atoms K
islvol5.v V = LVols K
Assertion islvol2 K HL X V X B p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s

Proof

Step Hyp Ref Expression
1 islvol5.b B = Base K
2 islvol5.l ˙ = K
3 islvol5.j ˙ = join K
4 islvol5.a A = Atoms K
5 islvol5.v V = LVols K
6 1 5 lvolbase X V X B
7 6 pm4.71ri X V X B X V
8 1 2 3 4 5 islvol5 K HL X B X V p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
9 8 pm5.32da K HL X B X V X B p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
10 7 9 syl5bb K HL X V X B p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s