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 ⁡ d q + 𝑃 ⁡ k f ⁡ q ∩ ⊥ 𝑃 ⁡ k ⁡ d = r + 𝑃 ⁡ k f ⁡ r ∩ ⊥ 𝑃 ⁡ k ⁡ d

Detailed syntax breakdown

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