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	eqtrid	⊢ ( 𝐾 ∈ 𝑉 → 𝐷 = ( ( 𝑤 ∈ 𝐻 ↦ { ⟨ ( 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 ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } )