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 ⊢ ≤ = ( le ‘ 𝐾 )
ltrnset.j ⊢ ∨ = ( join ‘ 𝐾 )
ltrnset.m ⊢ ∧ = ( meet ‘ 𝐾 )
ltrnset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ltrnset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion ltrnfset ( 𝐾 ∈ 𝐶 → ( LTrn ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } ) )

Proof

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