Metamath Proof Explorer

Theorem trlfset

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

Ref Expression
Hypotheses trlset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
trlset.l ⊢ ≤ = ( le ‘ 𝐾 )
trlset.j ⊢ ∨ = ( join ‘ 𝐾 )
trlset.m ⊢ ∧ = ( meet ‘ 𝐾 )
trlset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
trlset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion trlfset ( 𝐾 ∈ 𝐶 → ( trL ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 trlset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 trlset.l ⊢ ≤ = ( le ‘ 𝐾 )
3 trlset.j ⊢ ∨ = ( join ‘ 𝐾 )
4 trlset.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 trlset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 trlset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 elex ⊢ ( 𝐾 ∈ 𝐶 → 𝐾 ∈ V )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
9 8 6 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
10 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LTrn ‘ 𝑘 ) = ( LTrn ‘ 𝐾 ) )
11 10 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) )
12 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
13 12 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
14 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
15 14 5 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
16 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
17 16 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
18 17 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑝 ( le ‘ 𝑘 ) 𝑤 ↔ 𝑝 ≤ 𝑤 ) )
19 18 notbid ⊢ ( 𝑘 = 𝐾 → ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ↔ ¬ 𝑝 ≤ 𝑤 ) )
20 fveq2 ⊢ ( 𝑘 = 𝐾 → ( meet ‘ 𝑘 ) = ( meet ‘ 𝐾 ) )
21 20 4 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( meet ‘ 𝑘 ) = ∧ )
22 fveq2 ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ( join ‘ 𝐾 ) )
23 22 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ∨ )
24 23 oveqd ⊢ ( 𝑘 = 𝐾 → ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) = ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) )
25 eqidd ⊢ ( 𝑘 = 𝐾 → 𝑤 = 𝑤 )
26 21 24 25 oveq123d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) )
27 26 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ↔ 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) )
28 19 27 imbi12d ⊢ ( 𝑘 = 𝐾 → ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ↔ ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) )
29 15 28 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) )
30 13 29 riotaeqbidv ⊢ ( 𝑘 = 𝐾 → ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) = ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) )
31 11 30 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) )
32 9 31 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) )
33 df-trl ⊢ trL = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) )
34 32 33 6 mptfvmpt ⊢ ( 𝐾 ∈ V → ( trL ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) )
35 7 34 syl ⊢ ( 𝐾 ∈ 𝐶 → ( trL ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) )