Metamath Proof Explorer

Theorem tendoset

Description: The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom W . (Contributed by NM, 8-Jun-2013)

Ref Expression
Hypotheses tendoset.l ⊢ ≤ = ( le ‘ 𝐾 )
tendoset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoset.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
tendoset.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendoset ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } )

Proof

Step Hyp Ref Expression
1 tendoset.l ⊢ ≤ = ( le ‘ 𝐾 )
2 tendoset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendoset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendoset.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 tendoset.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 1 2 tendofset ⊢ ( 𝐾 ∈ 𝑉 → ( TEndo ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) )
7 6 fveq1d ⊢ ( 𝐾 ∈ 𝑉 → ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) ‘ 𝑊 ) )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
9 8 8 feq23d ⊢ ( 𝑤 = 𝑊 → ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↔ 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) )
10 8 raleqdv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ↔ ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ) )
11 8 10 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ) )
12 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) )
13 12 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) = 𝑅 )
14 13 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) = ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) )
15 13 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) = ( 𝑅 ‘ 𝑓 ) )
16 14 15 breq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ↔ ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) )
17 8 16 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) )
18 9 11 17 3anbi123d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) ↔ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) ) )
19 18 abbidv ⊢ ( 𝑤 = 𝑊 → { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } = { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } )
20 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } )
21 fvex ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
22 21 21 mapval ⊢ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↑m ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) = { 𝑠 ∣ 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) }
23 ovex ⊢ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↑m ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ V
24 22 23 eqeltrri ⊢ { 𝑠 ∣ 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) } ∈ V
25 simp1 ⊢ ( ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) → 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
26 25 ss2abi ⊢ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } ⊆ { 𝑠 ∣ 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) }
27 24 26 ssexi ⊢ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } ∈ V
28 19 20 27 fvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) ‘ 𝑊 ) = { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } )
29 3 3 feq23i ⊢ ( 𝑠 : 𝑇 ⟶ 𝑇 ↔ 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
30 3 raleqi ⊢ ( ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ↔ ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) )
31 3 30 raleqbii ⊢ ( ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) )
32 3 raleqi ⊢ ( ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) )
33 29 31 32 3anbi123i ⊢ ( ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) ↔ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) )
34 33 abbii ⊢ { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } = { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) }
35 28 34 eqtr4di ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) ‘ 𝑊 ) = { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } )
36 7 35 sylan9eq ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } )
37 5 36 eqtrid ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = { 𝑠 ∣ ( 𝑠 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑠 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑠 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑅 ‘ ( 𝑠 ‘ 𝑓 ) ) ≤ ( 𝑅 ‘ 𝑓 ) ) } )