Definition df-trnN 40109

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

Assertion

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

Distinct variable group:   𝑘,𝑑,𝑓,𝑞,𝑟

Detailed syntax breakdown of Definition df-trnN

Step	Hyp	Ref	Expression
1		ctrnN 40105	. 2 class Trn
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vd	. . . 4 setvar 𝑑
5	2	cv 1539	. . . . 5 class 𝑘
6		catm 39264	. . . . 5 class Atoms
7	5, 6	cfv 6561	. . . 4 class (Atoms‘𝑘)
8		vq	. . . . . . . . . . 11 setvar 𝑞
9	8	cv 1539	. . . . . . . . . 10 class 𝑞
10		vf	. . . . . . . . . . . 12 setvar 𝑓
11	10	cv 1539	. . . . . . . . . . 11 class 𝑓
12	9, 11	cfv 6561	. . . . . . . . . 10 class (𝑓‘𝑞)
13		cpadd 39797	. . . . . . . . . . 11 class +𝑃
14	5, 13	cfv 6561	. . . . . . . . . 10 class (+𝑃‘𝑘)
15	9, 12, 14	co 7431	. . . . . . . . 9 class (𝑞(+𝑃‘𝑘)(𝑓‘𝑞))
16	4	cv 1539	. . . . . . . . . . 11 class 𝑑
17	16	csn 4626	. . . . . . . . . 10 class {𝑑}
18		cpolN 39904	. . . . . . . . . . 11 class ⊥𝑃
19	5, 18	cfv 6561	. . . . . . . . . 10 class (⊥𝑃‘𝑘)
20	17, 19	cfv 6561	. . . . . . . . 9 class ((⊥𝑃‘𝑘)‘{𝑑})
21	15, 20	cin 3950	. . . . . . . 8 class ((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))
22		vr	. . . . . . . . . . 11 setvar 𝑟
23	22	cv 1539	. . . . . . . . . 10 class 𝑟
24	23, 11	cfv 6561	. . . . . . . . . 10 class (𝑓‘𝑟)
25	23, 24, 14	co 7431	. . . . . . . . 9 class (𝑟(+𝑃‘𝑘)(𝑓‘𝑟))
26	25, 20	cin 3950	. . . . . . . 8 class ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))
27	21, 26	wceq 1540	. . . . . . 7 wff ((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))
28		cwpointsN 39988	. . . . . . . . 9 class WAtoms
29	5, 28	cfv 6561	. . . . . . . 8 class (WAtoms‘𝑘)
30	16, 29	cfv 6561	. . . . . . 7 class ((WAtoms‘𝑘)‘𝑑)
31	27, 22, 30	wral 3061	. . . . . 6 wff ∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))
32	31, 8, 30	wral 3061	. . . . 5 wff ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))
33		cdilN 40104	. . . . . . 7 class Dil
34	5, 33	cfv 6561	. . . . . 6 class (Dil‘𝑘)
35	16, 34	cfv 6561	. . . . 5 class ((Dil‘𝑘)‘𝑑)
36	32, 10, 35	crab 3436	. . . 4 class {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))}
37	4, 7, 36	cmpt 5225	. . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))})
38	2, 3, 37	cmpt 5225	. 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))}))
39	1, 38	wceq 1540	1 wff Trn = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩ ((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩ ((⊥𝑃‘𝑘)‘{𝑑}))}))

This definition is referenced by:  trnfsetN  40157