Metamath Proof Explorer


Theorem lvoln0N

Description: A lattice volume is nonzero. (Contributed by NM, 17-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lvoln0.z 0 ˙ = 0. K
lvoln0.v V = LVols K
Assertion lvoln0N K HL X V X 0 ˙

Proof

Step Hyp Ref Expression
1 lvoln0.z 0 ˙ = 0. K
2 lvoln0.v V = LVols K
3 eqid Atoms K = Atoms K
4 3 atex K HL Atoms K
5 n0 Atoms K p p Atoms K
6 4 5 sylib K HL p p Atoms K
7 6 adantr K HL X V p p Atoms K
8 eqid K = K
9 8 3 2 lvolnleat K HL X V p Atoms K ¬ X K p
10 9 3expa K HL X V p Atoms K ¬ X K p
11 hlop K HL K OP
12 11 ad2antrr K HL X V p Atoms K K OP
13 eqid Base K = Base K
14 13 3 atbase p Atoms K p Base K
15 14 adantl K HL X V p Atoms K p Base K
16 13 8 1 op0le K OP p Base K 0 ˙ K p
17 12 15 16 syl2anc K HL X V p Atoms K 0 ˙ K p
18 breq1 X = 0 ˙ X K p 0 ˙ K p
19 17 18 syl5ibrcom K HL X V p Atoms K X = 0 ˙ X K p
20 19 necon3bd K HL X V p Atoms K ¬ X K p X 0 ˙
21 10 20 mpd K HL X V p Atoms K X 0 ˙
22 7 21 exlimddv K HL X V X 0 ˙