Definition df-tendo 38776

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

Assertion

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

Distinct variable group:   𝑤,𝑘,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-tendo

Step	Hyp	Ref	Expression
1		ctendo 38773	. 2 class TEndo
2		vk	. . 3 setvar 𝑘
3		cvv 3433	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 38005	. . . . 5 class LHyp
7	5, 6	cfv 6437	. . . 4 class (LHyp‘𝑘)
8	4	cv 1538	. . . . . . . 8 class 𝑤
9		cltrn 38122	. . . . . . . . 9 class LTrn
10	5, 9	cfv 6437	. . . . . . . 8 class (LTrn‘𝑘)
11	8, 10	cfv 6437	. . . . . . 7 class ((LTrn‘𝑘)‘𝑤)
12		vf	. . . . . . . 8 setvar 𝑓
13	12	cv 1538	. . . . . . 7 class 𝑓
14	11, 11, 13	wf 6433	. . . . . 6 wff 𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤)
15		vx	. . . . . . . . . . . 12 setvar 𝑥
16	15	cv 1538	. . . . . . . . . . 11 class 𝑥
17		vy	. . . . . . . . . . . 12 setvar 𝑦
18	17	cv 1538	. . . . . . . . . . 11 class 𝑦
19	16, 18	ccom 5594	. . . . . . . . . 10 class (𝑥 ∘ 𝑦)
20	19, 13	cfv 6437	. . . . . . . . 9 class (𝑓‘(𝑥 ∘ 𝑦))
21	16, 13	cfv 6437	. . . . . . . . . 10 class (𝑓‘𝑥)
22	18, 13	cfv 6437	. . . . . . . . . 10 class (𝑓‘𝑦)
23	21, 22	ccom 5594	. . . . . . . . 9 class ((𝑓‘𝑥) ∘ (𝑓‘𝑦))
24	20, 23	wceq 1539	. . . . . . . 8 wff (𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦))
25	24, 17, 11	wral 3065	. . . . . . 7 wff ∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦))
26	25, 15, 11	wral 3065	. . . . . 6 wff ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦))
27		ctrl 38179	. . . . . . . . . . 11 class trL
28	5, 27	cfv 6437	. . . . . . . . . 10 class (trL‘𝑘)
29	8, 28	cfv 6437	. . . . . . . . 9 class ((trL‘𝑘)‘𝑤)
30	21, 29	cfv 6437	. . . . . . . 8 class (((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))
31	16, 29	cfv 6437	. . . . . . . 8 class (((trL‘𝑘)‘𝑤)‘𝑥)
32		cple 16978	. . . . . . . . 9 class le
33	5, 32	cfv 6437	. . . . . . . 8 class (le‘𝑘)
34	30, 31, 33	wbr 5075	. . . . . . 7 wff (((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥)
35	34, 15, 11	wral 3065	. . . . . 6 wff ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥)
36	14, 26, 35	w3a 1086	. . . . 5 wff (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))
37	36, 12	cab 2716	. . . 4 class {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}
38	4, 7, 37	cmpt 5158	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))})
39	2, 3, 38	cmpt 5158	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}))
40	1, 39	wceq 1539	1 wff TEndo = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}))

This definition is referenced by:  tendofset  38779