This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = Base K
lvolset.c ⊢ C = ⋖ K
lvolset.p ⊢ P = LPlanes ⁡ K
lvolset.v ⊢ V = LVols ⁡ K
Assertion lvolset ⊢ K ∈ A → V = x ∈ B | ∃ y ∈ P y C x

Proof

Step Hyp Ref Expression
1 lvolset.b ⊢ B = Base K
2 lvolset.c ⊢ C = ⋖ K
3 lvolset.p ⊢ P = LPlanes ⁡ K
4 lvolset.v ⊢ V = LVols ⁡ K
5 elex ⊢ K ∈ A → K ∈ V
6 fveq2 ⊢ k = K → Base k = Base K
7 6 1 eqtr4di ⊢ k = K → Base k = B
8 fveq2 ⊢ k = K → LPlanes ⁡ k = LPlanes ⁡ K
9 8 3 eqtr4di ⊢ k = K → LPlanes ⁡ k = P
10 fveq2 ⊢ k = K → ⋖ k = ⋖ K
11 10 2 eqtr4di ⊢ k = K → ⋖ k = C
12 11 breqd ⊢ k = K → y ⋖ k x ↔ y C x
13 9 12 rexeqbidv ⊢ k = K → ∃ y ∈ LPlanes ⁡ k y ⋖ k x ↔ ∃ y ∈ P y C x
14 7 13 rabeqbidv ⊢ k = K → x ∈ Base k | ∃ y ∈ LPlanes ⁡ k y ⋖ k x = x ∈ B | ∃ y ∈ P y C x
15 df-lvols ⊢ LVols = k ∈ V ⟼ x ∈ Base k | ∃ y ∈ LPlanes ⁡ k y ⋖ k x
16 1 fvexi ⊢ B ∈ V
17 16 rabex ⊢ x ∈ B | ∃ y ∈ P y C x ∈ V
18 14 15 17 fvmpt ⊢ K ∈ V → LVols ⁡ K = x ∈ B | ∃ y ∈ P y C x
19 4 18 eqtrid ⊢ K ∈ V → V = x ∈ B | ∃ y ∈ P y C x
20 5 19 syl ⊢ K ∈ A → V = x ∈ B | ∃ y ∈ P y C x