Definition df-trnN

Description: Define set of all translations. Definition of translation in Crawley p. 111. (Contributed by NM, 4-Feb-2012)

	Ref	Expression
Assertion	df-trnN	⊢ Trn = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrnN	⊢ Trn
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		catm	⊢ Atoms
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( Atoms ‘ 𝑘 )
7		vf	⊢ 𝑓
8		cdilN	⊢ Dil
9	5 8	cfv	⊢ ( Dil ‘ 𝑘 )
10	3	cv	⊢ 𝑑
11	10 9	cfv	⊢ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 )
12		vq	⊢ 𝑞
13		cwpointsN	⊢ WAtoms
14	5 13	cfv	⊢ ( WAtoms ‘ 𝑘 )
15	10 14	cfv	⊢ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 )
16		vr	⊢ 𝑟
17	12	cv	⊢ 𝑞
18		cpadd	⊢ +𝑃
19	5 18	cfv	⊢ ( +𝑃 ‘ 𝑘 )
20	7	cv	⊢ 𝑓
21	17 20	cfv	⊢ ( 𝑓 ‘ 𝑞 )
22	17 21 19	co	⊢ ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) )
23		cpolN	⊢ ⊥𝑃
24	5 23	cfv	⊢ ( ⊥𝑃 ‘ 𝑘 )
25	10	csn	⊢ { 𝑑 }
26	25 24	cfv	⊢ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } )
27	22 26	cin	⊢ ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) )
28	16	cv	⊢ 𝑟
29	28 20	cfv	⊢ ( 𝑓 ‘ 𝑟 )
30	28 29 19	co	⊢ ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) )
31	30 26	cin	⊢ ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) )
32	27 31	wceq	⊢ ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) )
33	32 16 15	wral	⊢ ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) )
34	33 12 15	wral	⊢ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) )
35	34 7 11	crab	⊢ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) }
36	3 6 35	cmpt	⊢ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } )
37	1 2 36	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) )
38	0 37	wceq	⊢ Trn = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) )