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 = ( 𝑘 ∈ 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 ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃𝑘 ) ( 𝑓𝑞 ) ) ∩ ( ( ⊥𝑃𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃𝑘 ) ( 𝑓𝑟 ) ) ∩ ( ( ⊥𝑃𝑘 ) ‘ { 𝑑 } ) ) } ) )