# Metamath Proof Explorer

## Theorem lvolset

Description: The set of 3-dim lattice volumes in a Hilbert lattice. (Contributed by NM, 1-Jul-2012)

Ref Expression
Hypotheses lvolset.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
lvolset.c ${⊢}{C}={⋖}_{{K}}$
lvolset.p ${⊢}{P}=\mathrm{LPlanes}\left({K}\right)$
lvolset.v ${⊢}{V}=\mathrm{LVols}\left({K}\right)$
Assertion lvolset ${⊢}{K}\in {A}\to {V}=\left\{{x}\in {B}|\exists {y}\in {P}\phantom{\rule{.4em}{0ex}}{y}{C}{x}\right\}$

### Proof

Step Hyp Ref Expression
1 lvolset.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lvolset.c ${⊢}{C}={⋖}_{{K}}$
3 lvolset.p ${⊢}{P}=\mathrm{LPlanes}\left({K}\right)$
4 lvolset.v ${⊢}{V}=\mathrm{LVols}\left({K}\right)$
5 elex ${⊢}{K}\in {A}\to {K}\in \mathrm{V}$
6 fveq2 ${⊢}{k}={K}\to {\mathrm{Base}}_{{k}}={\mathrm{Base}}_{{K}}$
7 6 1 syl6eqr ${⊢}{k}={K}\to {\mathrm{Base}}_{{k}}={B}$
8 fveq2 ${⊢}{k}={K}\to \mathrm{LPlanes}\left({k}\right)=\mathrm{LPlanes}\left({K}\right)$
9 8 3 syl6eqr ${⊢}{k}={K}\to \mathrm{LPlanes}\left({k}\right)={P}$
10 fveq2 ${⊢}{k}={K}\to {⋖}_{{k}}={⋖}_{{K}}$
11 10 2 syl6eqr ${⊢}{k}={K}\to {⋖}_{{k}}={C}$
12 11 breqd ${⊢}{k}={K}\to \left({y}{⋖}_{{k}}{x}↔{y}{C}{x}\right)$
13 9 12 rexeqbidv ${⊢}{k}={K}\to \left(\exists {y}\in \mathrm{LPlanes}\left({k}\right)\phantom{\rule{.4em}{0ex}}{y}{⋖}_{{k}}{x}↔\exists {y}\in {P}\phantom{\rule{.4em}{0ex}}{y}{C}{x}\right)$
14 7 13 rabeqbidv ${⊢}{k}={K}\to \left\{{x}\in {\mathrm{Base}}_{{k}}|\exists {y}\in \mathrm{LPlanes}\left({k}\right)\phantom{\rule{.4em}{0ex}}{y}{⋖}_{{k}}{x}\right\}=\left\{{x}\in {B}|\exists {y}\in {P}\phantom{\rule{.4em}{0ex}}{y}{C}{x}\right\}$
15 df-lvols ${⊢}\mathrm{LVols}=\left({k}\in \mathrm{V}⟼\left\{{x}\in {\mathrm{Base}}_{{k}}|\exists {y}\in \mathrm{LPlanes}\left({k}\right)\phantom{\rule{.4em}{0ex}}{y}{⋖}_{{k}}{x}\right\}\right)$
16 1 fvexi ${⊢}{B}\in \mathrm{V}$
17 16 rabex ${⊢}\left\{{x}\in {B}|\exists {y}\in {P}\phantom{\rule{.4em}{0ex}}{y}{C}{x}\right\}\in \mathrm{V}$
18 14 15 17 fvmpt ${⊢}{K}\in \mathrm{V}\to \mathrm{LVols}\left({K}\right)=\left\{{x}\in {B}|\exists {y}\in {P}\phantom{\rule{.4em}{0ex}}{y}{C}{x}\right\}$
19 4 18 syl5eq ${⊢}{K}\in \mathrm{V}\to {V}=\left\{{x}\in {B}|\exists {y}\in {P}\phantom{\rule{.4em}{0ex}}{y}{C}{x}\right\}$
20 5 19 syl ${⊢}{K}\in {A}\to {V}=\left\{{x}\in {B}|\exists {y}\in {P}\phantom{\rule{.4em}{0ex}}{y}{C}{x}\right\}$