Metamath Proof Explorer


Theorem erngset-rN

Description: The division ring on trace-preserving endomorphisms for a fiducial co-atom W . (Contributed by NM, 5-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses erngset.h-r 𝐻 = ( LHyp ‘ 𝐾 )
erngset.t-r 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erngset.e-r 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erngset.d-r 𝐷 = ( ( EDRingR𝐾 ) ‘ 𝑊 )
Assertion erngset-rN ( ( 𝐾𝑉𝑊𝐻 ) → 𝐷 = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } )

Proof

Step Hyp Ref Expression
1 erngset.h-r 𝐻 = ( LHyp ‘ 𝐾 )
2 erngset.t-r 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erngset.e-r 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 erngset.d-r 𝐷 = ( ( EDRingR𝐾 ) ‘ 𝑊 )
5 1 erngfset-rN ( 𝐾𝑉 → ( EDRingR𝐾 ) = ( 𝑤𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } ) )
6 5 fveq1d ( 𝐾𝑉 → ( ( EDRingR𝐾 ) ‘ 𝑊 ) = ( ( 𝑤𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } ) ‘ 𝑊 ) )
7 4 6 syl5eq ( 𝐾𝑉𝐷 = ( ( 𝑤𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } ) ‘ 𝑊 ) )
8 fveq2 ( 𝑤 = 𝑊 → ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
9 8 opeq2d ( 𝑤 = 𝑊 → ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩ )
10 tpeq1 ( ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩ → { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } )
11 3 opeq2i ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ = ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩
12 tpeq1 ( ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ = ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩ → { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } )
13 11 12 ax-mp { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ }
14 10 13 eqtr4di ( ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟩ → { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } )
15 9 14 syl ( 𝑤 = 𝑊 → { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } )
16 8 3 eqtr4di ( 𝑤 = 𝑊 → ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) = 𝐸 )
17 fveq2 ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
18 17 2 eqtr4di ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = 𝑇 )
19 eqidd ( 𝑤 = 𝑊 → ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) )
20 18 19 mpteq12dv ( 𝑤 = 𝑊 → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) = ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) )
21 16 16 20 mpoeq123dv ( 𝑤 = 𝑊 → ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) )
22 21 opeq2d ( 𝑤 = 𝑊 → ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ )
23 22 tpeq2d ( 𝑤 = 𝑊 → { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } )
24 eqidd ( 𝑤 = 𝑊 → ( 𝑡𝑠 ) = ( 𝑡𝑠 ) )
25 16 16 24 mpoeq123dv ( 𝑤 = 𝑊 → ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) )
26 25 opeq2d ( 𝑤 = 𝑊 → ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ = ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ )
27 26 tpeq3d ( 𝑤 = 𝑊 → { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } )
28 15 23 27 3eqtrd ( 𝑤 = 𝑊 → { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } )
29 eqid ( 𝑤𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } ) = ( 𝑤𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } )
30 tpex { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } ∈ V
31 28 29 30 fvmpt ( 𝑊𝐻 → ( ( 𝑤𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑡𝑠 ) ) ⟩ } ) ‘ 𝑊 ) = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } )
32 7 31 sylan9eq ( ( 𝐾𝑉𝑊𝐻 ) → 𝐷 = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } )