Metamath Proof Explorer

Definition df-tendo

Description: Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013)

Ref Expression
Assertion df-tendo TEndo = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∣ ( 𝑓 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctendo ⊢ TEndo
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 vf ⊢ 𝑓
8 7 cv ⊢ 𝑓
9 cltrn ⊢ LTrn
10 5 9 cfv ⊢ ( LTrn ‘ 𝑘 )
11 3 cv ⊢ 𝑤
12 11 10 cfv ⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
13 12 12 8 wf ⊢ 𝑓 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
14 vx ⊢ 𝑥
15 vy ⊢ 𝑦
16 14 cv ⊢ 𝑥
17 15 cv ⊢ 𝑦
18 16 17 ccom ⊢ ( 𝑥 ∘ 𝑦 )
19 18 8 cfv ⊢ ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) )
20 16 8 cfv ⊢ ( 𝑓 ‘ 𝑥 )
21 17 8 cfv ⊢ ( 𝑓 ‘ 𝑦 )
22 20 21 ccom ⊢ ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) )
23 19 22 wceq ⊢ ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) )
24 23 15 12 wral ⊢ ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) )
25 24 14 12 wral ⊢ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) )
26 ctrl ⊢ trL
27 5 26 cfv ⊢ ( trL ‘ 𝑘 )
28 11 27 cfv ⊢ ( ( trL ‘ 𝑘 ) ‘ 𝑤 )
29 20 28 cfv ⊢ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) )
30 cple ⊢ le
31 5 30 cfv ⊢ ( le ‘ 𝑘 )
32 16 28 cfv ⊢ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 )
33 29 32 31 wbr ⊢ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 )
34 33 14 12 wral ⊢ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 )
35 13 25 34 w3a ⊢ ( 𝑓 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) )
36 35 7 cab ⊢ { 𝑓 ∣ ( 𝑓 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ) }
37 3 6 36 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∣ ( 𝑓 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ) } )
38 1 2 37 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∣ ( 𝑓 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ) } ) )
39 0 38 wceq ⊢ TEndo = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∣ ( 𝑓 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑦 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑓 ‘ ( 𝑥 ∘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ∘ ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ) } ) )