This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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