Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  erngset Structured version   Visualization version   GIF version

Theorem erngset 39201
Description: The division ring on trace-preserving endomorphisms for a fiducial co-atom π‘Š. (Contributed by NM, 5-Jun-2013.)
Hypotheses
Ref Expression
erngset.h 𝐻 = (LHypβ€˜πΎ)
erngset.t 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
erngset.e 𝐸 = ((TEndoβ€˜πΎ)β€˜π‘Š)
erngset.d 𝐷 = ((EDRingβ€˜πΎ)β€˜π‘Š)
Assertion
Ref Expression
erngset ((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) β†’ 𝐷 = {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑))⟩})
Distinct variable groups:   𝑓,𝑠,𝑑,𝐾   𝑓,π‘Š,𝑠,𝑑
Allowed substitution hints:   𝐷(𝑑,𝑓,𝑠)   𝑇(𝑑,𝑓,𝑠)   𝐸(𝑑,𝑓,𝑠)   𝐻(𝑑,𝑓,𝑠)   𝑉(𝑑,𝑓,𝑠)

Proof of Theorem erngset
Dummy variable 𝑀 is distinct from all other variables.
StepHypRef Expression
1 erngset.d . . 3 𝐷 = ((EDRingβ€˜πΎ)β€˜π‘Š)
2 erngset.h . . . . 5 𝐻 = (LHypβ€˜πΎ)
32erngfset 39200 . . . 4 (𝐾 ∈ 𝑉 β†’ (EDRingβ€˜πΎ) = (𝑀 ∈ 𝐻 ↦ {⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩}))
43fveq1d 6841 . . 3 (𝐾 ∈ 𝑉 β†’ ((EDRingβ€˜πΎ)β€˜π‘Š) = ((𝑀 ∈ 𝐻 ↦ {⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})β€˜π‘Š))
51, 4eqtrid 2789 . 2 (𝐾 ∈ 𝑉 β†’ 𝐷 = ((𝑀 ∈ 𝐻 ↦ {⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})β€˜π‘Š))
6 fveq2 6839 . . . . . 6 (𝑀 = π‘Š β†’ ((TEndoβ€˜πΎ)β€˜π‘€) = ((TEndoβ€˜πΎ)β€˜π‘Š))
76opeq2d 4835 . . . . 5 (𝑀 = π‘Š β†’ ⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘€)⟩ = ⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘Š)⟩)
8 tpeq1 4701 . . . . . 6 (⟨(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β€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})
9 erngset.e . . . . . . . 8 𝐸 = ((TEndoβ€˜πΎ)β€˜π‘Š)
109opeq2i 4832 . . . . . . 7 ⟨(Baseβ€˜ndx), 𝐸⟩ = ⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘Š)⟩
11 tpeq1 4701 . . . . . . 7 (⟨(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β€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})
1210, 11ax-mp 5 . . . . . 6 {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩} = {⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘Š)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩}
138, 12eqtr4di 2795 . . . . 5 (⟨(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β€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})
147, 13syl 17 . . . 4 (𝑀 = π‘Š β†’ {⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩} = {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})
156, 9eqtr4di 2795 . . . . . . 7 (𝑀 = π‘Š β†’ ((TEndoβ€˜πΎ)β€˜π‘€) = 𝐸)
16 fveq2 6839 . . . . . . . . 9 (𝑀 = π‘Š β†’ ((LTrnβ€˜πΎ)β€˜π‘€) = ((LTrnβ€˜πΎ)β€˜π‘Š))
17 erngset.t . . . . . . . . 9 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
1816, 17eqtr4di 2795 . . . . . . . 8 (𝑀 = π‘Š β†’ ((LTrnβ€˜πΎ)β€˜π‘€) = 𝑇)
19 eqidd 2738 . . . . . . . 8 (𝑀 = π‘Š β†’ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“)) = ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“)))
2018, 19mpteq12dv 5194 . . . . . . 7 (𝑀 = π‘Š β†’ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))) = (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))
2115, 15, 20mpoeq123dv 7426 . . . . . 6 (𝑀 = π‘Š β†’ (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“)))) = (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“)))))
2221opeq2d 4835 . . . . 5 (𝑀 = π‘Š β†’ ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩ = ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩)
2322tpeq2d 4705 . . . 4 (𝑀 = π‘Š β†’ {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩} = {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})
24 eqidd 2738 . . . . . . 7 (𝑀 = π‘Š β†’ (𝑠 ∘ 𝑑) = (𝑠 ∘ 𝑑))
2515, 15, 24mpoeq123dv 7426 . . . . . 6 (𝑀 = π‘Š β†’ (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑)) = (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑)))
2625opeq2d 4835 . . . . 5 (𝑀 = π‘Š β†’ ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩ = ⟨(.rβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑))⟩)
2726tpeq3d 4706 . . . 4 (𝑀 = π‘Š β†’ {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩} = {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑))⟩})
2814, 23, 273eqtrd 2781 . . 3 (𝑀 = π‘Š β†’ {⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩} = {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑))⟩})
29 eqid 2737 . . 3 (𝑀 ∈ 𝐻 ↦ {⟨(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 7673 . . 3 {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑))⟩} ∈ V
3128, 29, 30fvmpt 6945 . 2 (π‘Š ∈ 𝐻 β†’ ((𝑀 ∈ 𝐻 ↦ {⟨(Baseβ€˜ndx), ((TEndoβ€˜πΎ)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜πΎ)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜πΎ)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜πΎ)β€˜π‘€) ↦ (𝑠 ∘ 𝑑))⟩})β€˜π‘Š) = {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑))⟩})
325, 31sylan9eq 2797 1 ((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) β†’ 𝐷 = {⟨(Baseβ€˜ndx), 𝐸⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ 𝐸, 𝑑 ∈ 𝐸 ↦ (𝑠 ∘ 𝑑))⟩})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {ctp 4588  βŸ¨cop 4590   ↦ cmpt 5186   ∘ ccom 5635  β€˜cfv 6493   ∈ cmpo 7353  ndxcnx 17025  Basecbs 17043  +gcplusg 17093  .rcmulr 17094  LHypclh 38385  LTrncltrn 38502  TEndoctendo 39153  EDRingcedring 39154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-oprab 7355  df-mpo 7356  df-edring 39158
This theorem is referenced by:  erngbase  39202  erngfplus  39203  erngfmul  39206
  Copyright terms: Public domain W3C validator