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

Metamath Proof Explorer

Definition df-ltrn

Description: Define set of all lattice translations. Similar to definition of translation in Crawley p. 111. (Contributed by NM, 11-May-2012)

Ref Expression
Assertion df-ltrn LTrn = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( LDil ‘ 𝑘 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltrn ⊢ LTrn
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 vf ⊢ 𝑓
8 cldil ⊢ LDil
9 5 8 cfv ⊢ ( LDil ‘ 𝑘 )
10 3 cv ⊢ 𝑤
11 10 9 cfv ⊢ ( ( LDil ‘ 𝑘 ) ‘ 𝑤 )
12 vp ⊢ 𝑝
13 catm ⊢ Atoms
14 5 13 cfv ⊢ ( Atoms ‘ 𝑘 )
15 vq ⊢ 𝑞
16 12 cv ⊢ 𝑝
17 cple ⊢ le
18 5 17 cfv ⊢ ( le ‘ 𝑘 )
19 16 10 18 wbr ⊢ 𝑝 ( le ‘ 𝑘 ) 𝑤
20 19 wn ⊢ ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤
21 15 cv ⊢ 𝑞
22 21 10 18 wbr ⊢ 𝑞 ( le ‘ 𝑘 ) 𝑤
23 22 wn ⊢ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤
24 20 23 wa ⊢ ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 )
25 cjn ⊢ join
26 5 25 cfv ⊢ ( join ‘ 𝑘 )
27 7 cv ⊢ 𝑓
28 16 27 cfv ⊢ ( 𝑓 ‘ 𝑝 )
29 16 28 26 co ⊢ ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) )
30 cmee ⊢ meet
31 5 30 cfv ⊢ ( meet ‘ 𝑘 )
32 29 10 31 co ⊢ ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 )
33 21 27 cfv ⊢ ( 𝑓 ‘ 𝑞 )
34 21 33 26 co ⊢ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) )
35 34 10 31 co ⊢ ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 )
36 32 35 wceq ⊢ ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 )
37 24 36 wi ⊢ ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) )
38 37 15 14 wral ⊢ ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) )
39 38 12 14 wral ⊢ ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) )
40 39 7 11 crab ⊢ { 𝑓 ∈ ( ( LDil ‘ 𝑘 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) }
41 3 6 40 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( LDil ‘ 𝑘 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) } )
42 1 2 41 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( LDil ‘ 𝑘 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) } ) )
43 0 42 wceq ⊢ LTrn = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( LDil ‘ 𝑘 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 ∧ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ) → ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( 𝑞 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) } ) )