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 ‘ 𝑘 ) 𝑤 ) ) } ) )