Metamath Proof Explorer

Theorem ltrnfset

Description: The set of all lattice translations for a lattice K . (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses ltrnset.l ⊢ ≤ ˙ = ≤ K
ltrnset.j ⊢ ∨ ˙ = join ⁡ K
ltrnset.m ⊢ ∧ ˙ = meet ⁡ K
ltrnset.a ⊢ A = Atoms ⁡ K
ltrnset.h ⊢ H = LHyp ⁡ K
Assertion ltrnfset ⊢ K ∈ C → LTrn ⁡ K = w ∈ H ⟼ f ∈ LDil ⁡ K ⁡ w | ∀ p ∈ A ∀ q ∈ A ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w

Proof

Step Hyp Ref Expression
1 ltrnset.l ⊢ ≤ ˙ = ≤ K
2 ltrnset.j ⊢ ∨ ˙ = join ⁡ K
3 ltrnset.m ⊢ ∧ ˙ = meet ⁡ K
4 ltrnset.a ⊢ A = Atoms ⁡ K
5 ltrnset.h ⊢ H = LHyp ⁡ K
6 elex ⊢ K ∈ C → K ∈ V
7 fveq2 ⊢ k = K → LHyp ⁡ k = LHyp ⁡ K
8 7 5 eqtr4di ⊢ k = K → LHyp ⁡ k = H
9 fveq2 ⊢ k = K → LDil ⁡ k = LDil ⁡ K
10 9 fveq1d ⊢ k = K → LDil ⁡ k ⁡ w = LDil ⁡ K ⁡ w
11 fveq2 ⊢ k = K → Atoms ⁡ k = Atoms ⁡ K
12 11 4 eqtr4di ⊢ k = K → Atoms ⁡ k = A
13 fveq2 ⊢ k = K → ≤ k = ≤ K
14 13 1 eqtr4di ⊢ k = K → ≤ k = ≤ ˙
15 14 breqd ⊢ k = K → p ≤ k w ↔ p ≤ ˙ w
16 15 notbid ⊢ k = K → ¬ p ≤ k w ↔ ¬ p ≤ ˙ w
17 14 breqd ⊢ k = K → q ≤ k w ↔ q ≤ ˙ w
18 17 notbid ⊢ k = K → ¬ q ≤ k w ↔ ¬ q ≤ ˙ w
19 16 18 anbi12d ⊢ k = K → ¬ p ≤ k w ∧ ¬ q ≤ k w ↔ ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w
20 fveq2 ⊢ k = K → meet ⁡ k = meet ⁡ K
21 20 3 eqtr4di ⊢ k = K → meet ⁡ k = ∧ ˙
22 fveq2 ⊢ k = K → join ⁡ k = join ⁡ K
23 22 2 eqtr4di ⊢ k = K → join ⁡ k = ∨ ˙
24 23 oveqd ⊢ k = K → p join ⁡ k f ⁡ p = p ∨ ˙ f ⁡ p
25 eqidd ⊢ k = K → w = w
26 21 24 25 oveq123d ⊢ k = K → p join ⁡ k f ⁡ p meet ⁡ k w = p ∨ ˙ f ⁡ p ∧ ˙ w
27 23 oveqd ⊢ k = K → q join ⁡ k f ⁡ q = q ∨ ˙ f ⁡ q
28 21 27 25 oveq123d ⊢ k = K → q join ⁡ k f ⁡ q meet ⁡ k w = q ∨ ˙ f ⁡ q ∧ ˙ w
29 26 28 eqeq12d ⊢ k = K → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w ↔ p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w
30 19 29 imbi12d ⊢ k = K → ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w ↔ ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w
31 12 30 raleqbidv ⊢ k = K → ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w ↔ ∀ q ∈ A ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w
32 12 31 raleqbidv ⊢ k = K → ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w ↔ ∀ p ∈ A ∀ q ∈ A ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w
33 10 32 rabeqbidv ⊢ k = K → f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w = f ∈ LDil ⁡ K ⁡ w | ∀ p ∈ A ∀ q ∈ A ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w
34 8 33 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w = w ∈ H ⟼ f ∈ LDil ⁡ K ⁡ w | ∀ p ∈ A ∀ q ∈ A ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w
35 df-ltrn ⊢ LTrn = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LDil ⁡ k ⁡ w | ∀ p ∈ Atoms ⁡ k ∀ q ∈ Atoms ⁡ k ¬ p ≤ k w ∧ ¬ q ≤ k w → p join ⁡ k f ⁡ p meet ⁡ k w = q join ⁡ k f ⁡ q meet ⁡ k w
36 34 35 5 mptfvmpt ⊢ K ∈ V → LTrn ⁡ K = w ∈ H ⟼ f ∈ LDil ⁡ K ⁡ w | ∀ p ∈ A ∀ q ∈ A ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w
37 6 36 syl ⊢ K ∈ C → LTrn ⁡ K = w ∈ H ⟼ f ∈ LDil ⁡ K ⁡ w | ∀ p ∈ A ∀ q ∈ A ¬ p ≤ ˙ w ∧ ¬ q ≤ ˙ w → p ∨ ˙ f ⁡ p ∧ ˙ w = q ∨ ˙ f ⁡ q ∧ ˙ w