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

Metamath Proof Explorer

Theorem lhpset

Description: The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses lhpset.b ⊢ B = Base K
lhpset.u ⊢ 1 ˙ = 1. ⁡ K
lhpset.c ⊢ C = ⋖ K
lhpset.h ⊢ H = LHyp ⁡ K
Assertion lhpset ⊢ K ∈ A → H = w ∈ B | w C 1 ˙

Proof

Step Hyp Ref Expression
1 lhpset.b ⊢ B = Base K
2 lhpset.u ⊢ 1 ˙ = 1. ⁡ K
3 lhpset.c ⊢ C = ⋖ K
4 lhpset.h ⊢ H = LHyp ⁡ 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 eqidd ⊢ k = K → w = w
9 fveq2 ⊢ k = K → ⋖ k = ⋖ K
10 9 3 eqtr4di ⊢ k = K → ⋖ k = C
11 fveq2 ⊢ k = K → 1. ⁡ k = 1. ⁡ K
12 11 2 eqtr4di ⊢ k = K → 1. ⁡ k = 1 ˙
13 8 10 12 breq123d ⊢ k = K → w ⋖ k 1. ⁡ k ↔ w C 1 ˙
14 7 13 rabeqbidv ⊢ k = K → w ∈ Base k | w ⋖ k 1. ⁡ k = w ∈ B | w C 1 ˙
15 df-lhyp ⊢ LHyp = k ∈ V ⟼ w ∈ Base k | w ⋖ k 1. ⁡ k
16 1 fvexi ⊢ B ∈ V
17 16 rabex ⊢ w ∈ B | w C 1 ˙ ∈ V
18 14 15 17 fvmpt ⊢ K ∈ V → LHyp ⁡ K = w ∈ B | w C 1 ˙
19 4 18 eqtrid ⊢ K ∈ V → H = w ∈ B | w C 1 ˙
20 5 19 syl ⊢ K ∈ A → H = w ∈ B | w C 1 ˙