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 syl5eq ( ( 𝐾𝑉𝑊𝐻 ) → 𝐸 = { 𝑠 ∣ ( 𝑠 : 𝑇𝑇 ∧ ∀ 𝑓𝑇𝑔𝑇 ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓𝑇 ( 𝑅 ‘ ( 𝑠𝑓 ) ) ( 𝑅𝑓 ) ) } )