# Metamath Proof Explorer

## Theorem lvolcmp

Description: If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012)

Ref Expression
Hypotheses lvolcmp.l
lvolcmp.v ${⊢}{V}=\mathrm{LVols}\left({K}\right)$
Assertion lvolcmp

### Proof

Step Hyp Ref Expression
1 lvolcmp.l
2 lvolcmp.v ${⊢}{V}=\mathrm{LVols}\left({K}\right)$
3 simp2 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to {X}\in {V}$
4 simp1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to {K}\in \mathrm{HL}$
5 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
6 5 2 lvolbase ${⊢}{X}\in {V}\to {X}\in {\mathrm{Base}}_{{K}}$
7 6 3ad2ant2 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to {X}\in {\mathrm{Base}}_{{K}}$
8 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
9 eqid ${⊢}\mathrm{LPlanes}\left({K}\right)=\mathrm{LPlanes}\left({K}\right)$
10 5 8 9 2 islvol4 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {\mathrm{Base}}_{{K}}\right)\to \left({X}\in {V}↔\exists {z}\in \mathrm{LPlanes}\left({K}\right)\phantom{\rule{.4em}{0ex}}{z}{⋖}_{{K}}{X}\right)$
11 4 7 10 syl2anc ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to \left({X}\in {V}↔\exists {z}\in \mathrm{LPlanes}\left({K}\right)\phantom{\rule{.4em}{0ex}}{z}{⋖}_{{K}}{X}\right)$
12 3 11 mpbid ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to \exists {z}\in \mathrm{LPlanes}\left({K}\right)\phantom{\rule{.4em}{0ex}}{z}{⋖}_{{K}}{X}$
13 simpr3
14 hlpos ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Poset}$
15 14 3ad2ant1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {V}\wedge {Y}\in {V}\right)\to {K}\in \mathrm{Poset}$
18 simpl3
19 5 2 lvolbase ${⊢}{Y}\in {V}\to {Y}\in {\mathrm{Base}}_{{K}}$
20 18 19 syl
21 simpr1
22 5 9 lplnbase ${⊢}{z}\in \mathrm{LPlanes}\left({K}\right)\to {z}\in {\mathrm{Base}}_{{K}}$
23 21 22 syl
24 simpr2
25 simpl1
26 5 1 8 cvrle
27 25 23 17 24 26 syl31anc
28 5 1 postr
29 16 23 17 20 28 syl13anc
30 27 13 29 mp2and
31 1 8 9 2 lplncvrlvol2
32 25 21 18 30 31 syl31anc
33 5 1 8 cvrcmp
34 16 17 20 23 24 32 33 syl132anc
35 13 34 mpbid
36 35 3exp2
37 36 rexlimdv
38 12 37 mpd
39 5 1 posref
40 15 7 39 syl2anc
41 breq2
42 40 41 syl5ibcom
43 38 42 impbid