Metamath Proof Explorer

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=k∈V⟼d∈Atoms⁡k⟼f∈Dil⁡k⁡d|∀q∈WAtoms⁡k⁡d∀r∈WAtoms⁡k⁡dq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrnN classTrn
1 vk setvark
2 cvv classV
3 vd setvard
4 catm classAtoms
5 1 cv setvark
6 5 4 cfv classAtoms⁡k
7 vf setvarf
8 cdilN classDil
9 5 8 cfv classDil⁡k
10 3 cv setvard
11 10 9 cfv classDil⁡k⁡d
12 vq setvarq
13 cwpointsN classWAtoms
14 5 13 cfv classWAtoms⁡k
15 10 14 cfv classWAtoms⁡k⁡d
16 vr setvarr
17 12 cv setvarq
18 cpadd class+𝑃
19 5 18 cfv class+𝑃⁡k
20 7 cv setvarf
21 17 20 cfv classf⁡q
22 17 21 19 co classq+𝑃⁡kf⁡q
23 cpolN class⊥𝑃
24 5 23 cfv class⊥𝑃⁡k
25 10 csn classd
26 25 24 cfv class⊥𝑃⁡k⁡d
27 22 26 cin classq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d
28 16 cv setvarr
29 28 20 cfv classf⁡r
30 28 29 19 co classr+𝑃⁡kf⁡r
31 30 26 cin classr+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d
32 27 31 wceq wffq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d
33 32 16 15 wral wff∀r∈WAtoms⁡k⁡dq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d
34 33 12 15 wral wff∀q∈WAtoms⁡k⁡d∀r∈WAtoms⁡k⁡dq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d
35 34 7 11 crab classf∈Dil⁡k⁡d|∀q∈WAtoms⁡k⁡d∀r∈WAtoms⁡k⁡dq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d
36 3 6 35 cmpt classd∈Atoms⁡k⟼f∈Dil⁡k⁡d|∀q∈WAtoms⁡k⁡d∀r∈WAtoms⁡k⁡dq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d
37 1 2 36 cmpt classk∈V⟼d∈Atoms⁡k⟼f∈Dil⁡k⁡d|∀q∈WAtoms⁡k⁡d∀r∈WAtoms⁡k⁡dq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d
38 0 37 wceq wffTrn=k∈V⟼d∈Atoms⁡k⟼f∈Dil⁡k⁡d|∀q∈WAtoms⁡k⁡d∀r∈WAtoms⁡k⁡dq+𝑃⁡kf⁡q∩⊥𝑃⁡k⁡d=r+𝑃⁡kf⁡r∩⊥𝑃⁡k⁡d