Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trnN Structured version   Visualization version   GIF version

Definition df-trnN 38117
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
StepHypRef Expression
1 ctrnN 38113 . 2 class Trn
2 vk . . 3 setvar 𝑘
3 cvv 3431 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1541 . . . . 5 class 𝑘
6 catm 37273 . . . . 5 class Atoms
75, 6cfv 6432 . . . 4 class (Atoms‘𝑘)
8 vq . . . . . . . . . . 11 setvar 𝑞
98cv 1541 . . . . . . . . . 10 class 𝑞
10 vf . . . . . . . . . . . 12 setvar 𝑓
1110cv 1541 . . . . . . . . . . 11 class 𝑓
129, 11cfv 6432 . . . . . . . . . 10 class (𝑓𝑞)
13 cpadd 37805 . . . . . . . . . . 11 class +𝑃
145, 13cfv 6432 . . . . . . . . . 10 class (+𝑃𝑘)
159, 12, 14co 7271 . . . . . . . . 9 class (𝑞(+𝑃𝑘)(𝑓𝑞))
164cv 1541 . . . . . . . . . . 11 class 𝑑
1716csn 4567 . . . . . . . . . 10 class {𝑑}
18 cpolN 37912 . . . . . . . . . . 11 class 𝑃
195, 18cfv 6432 . . . . . . . . . 10 class (⊥𝑃𝑘)
2017, 19cfv 6432 . . . . . . . . 9 class ((⊥𝑃𝑘)‘{𝑑})
2115, 20cin 3891 . . . . . . . 8 class ((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑}))
22 vr . . . . . . . . . . 11 setvar 𝑟
2322cv 1541 . . . . . . . . . 10 class 𝑟
2423, 11cfv 6432 . . . . . . . . . 10 class (𝑓𝑟)
2523, 24, 14co 7271 . . . . . . . . 9 class (𝑟(+𝑃𝑘)(𝑓𝑟))
2625, 20cin 3891 . . . . . . . 8 class ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))
2721, 26wceq 1542 . . . . . . 7 wff ((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑})) = ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))
28 cwpointsN 37996 . . . . . . . . 9 class WAtoms
295, 28cfv 6432 . . . . . . . 8 class (WAtoms‘𝑘)
3016, 29cfv 6432 . . . . . . 7 class ((WAtoms‘𝑘)‘𝑑)
3127, 22, 30wral 3066 . . . . . 6 wff 𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑})) = ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))
3231, 8, 30wral 3066 . . . . 5 wff 𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑})) = ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))
33 cdilN 38112 . . . . . . 7 class Dil
345, 33cfv 6432 . . . . . 6 class (Dil‘𝑘)
3516, 34cfv 6432 . . . . 5 class ((Dil‘𝑘)‘𝑑)
3632, 10, 35crab 3070 . . . 4 class {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑})) = ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))}
374, 7, 36cmpt 5162 . . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑})) = ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))})
382, 3, 37cmpt 5162 . 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑})) = ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))}))
391, 38wceq 1542 1 wff Trn = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃𝑘)(𝑓𝑞)) ∩ ((⊥𝑃𝑘)‘{𝑑})) = ((𝑟(+𝑃𝑘)(𝑓𝑟)) ∩ ((⊥𝑃𝑘)‘{𝑑}))}))
Colors of variables: wff setvar class
This definition is referenced by:  trnfsetN  38165
  Copyright terms: Public domain W3C validator