Step | Hyp | Ref
| Expression |
1 | | elex 3450 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | fveq2 6774 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | erngset.h-r |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | eqtr4di 2796 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (TEndo‘𝑘) = (TEndo‘𝐾)) |
6 | 5 | fveq1d 6776 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((TEndo‘𝑘)‘𝑤) = ((TEndo‘𝐾)‘𝑤)) |
7 | 6 | opeq2d 4811 |
. . . . 5
⊢ (𝑘 = 𝐾 → 〈(Base‘ndx),
((TEndo‘𝑘)‘𝑤)〉 = 〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉) |
8 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
9 | 8 | fveq1d 6776 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
10 | 9 | mpteq1d 5169 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) |
11 | 6, 6, 10 | mpoeq123dv 7350 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))) |
12 | 11 | opeq2d 4811 |
. . . . 5
⊢ (𝑘 = 𝐾 → 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉 = 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉) |
13 | | eqidd 2739 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑡 ∘ 𝑠) = (𝑡 ∘ 𝑠)) |
14 | 6, 6, 13 | mpoeq123dv 7350 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑡 ∘ 𝑠))) |
15 | 14 | opeq2d 4811 |
. . . . 5
⊢ (𝑘 = 𝐾 → 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉 = 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉) |
16 | 7, 12, 15 | tpeq123d 4684 |
. . . 4
⊢ (𝑘 = 𝐾 → {〈(Base‘ndx),
((TEndo‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉} = {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉}) |
17 | 4, 16 | mpteq12dv 5165 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ {〈(Base‘ndx),
((TEndo‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉}) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉})) |
18 | | df-edring-rN 38770 |
. . 3
⊢
EDRingR = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {〈(Base‘ndx),
((TEndo‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉})) |
19 | 17, 18, 3 | mptfvmpt 7104 |
. 2
⊢ (𝐾 ∈ V →
(EDRingR‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉})) |
20 | 1, 19 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (EDRingR‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉})) |