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. ‘ 𝐾 )
lvoln0.v 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvoln0N ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) → 𝑋0 )

Proof

Step Hyp Ref Expression
1 lvoln0.z 0 = ( 0. ‘ 𝐾 )
2 lvoln0.v 𝑉 = ( LVols ‘ 𝐾 )
3 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
4 3 atex ( 𝐾 ∈ HL → ( Atoms ‘ 𝐾 ) ≠ ∅ )
5 n0 ( ( Atoms ‘ 𝐾 ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
6 4 5 sylib ( 𝐾 ∈ HL → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
7 6 adantr ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
8 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 8 3 2 lvolnleat ( ( 𝐾 ∈ HL ∧ 𝑋𝑉𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 )
10 9 3expa ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 )
11 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
12 11 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP )
13 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 3 atbase ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
15 14 adantl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
16 13 8 1 op0le ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 )
17 12 15 16 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 )
18 breq1 ( 𝑋 = 0 → ( 𝑋 ( le ‘ 𝐾 ) 𝑝0 ( le ‘ 𝐾 ) 𝑝 ) )
19 17 18 syl5ibrcom ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 = 0𝑋 ( le ‘ 𝐾 ) 𝑝 ) )
20 19 necon3bd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝𝑋0 ) )
21 10 20 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋0 )
22 7 21 exlimddv ( ( 𝐾 ∈ HL ∧ 𝑋𝑉 ) → 𝑋0 )