Metamath Proof Explorer

Theorem erngset

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

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

Proof

Step Hyp Ref Expression
1 erngset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 erngset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erngset.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 erngset.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
5 1 erngfset ⊢ ( 𝐾 ∈ 𝑉 → ( EDRing ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( 𝑠 ∘ 𝑡 ) ) ⟩ } ) )
6 5 fveq1d ⊢ ( 𝐾 ∈ 𝑉 → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( 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 ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑠 ∘ 𝑡 ) ) ⟩ } )