| Step | Hyp | Ref
| Expression |
| 1 | | erngset.d |
. . 3
⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) |
| 2 | | erngset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 3 | 2 | erngfset 40801 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (EDRing‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉})) |
| 4 | 3 | fveq1d 6908 |
. . 3
⊢ (𝐾 ∈ 𝑉 → ((EDRing‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉})‘𝑊)) |
| 5 | 1, 4 | eqtrid 2789 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐷 = ((𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉})‘𝑊)) |
| 6 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((TEndo‘𝐾)‘𝑤) = ((TEndo‘𝐾)‘𝑊)) |
| 7 | 6 | opeq2d 4880 |
. . . . 5
⊢ (𝑤 = 𝑊 → 〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉 = 〈(Base‘ndx),
((TEndo‘𝐾)‘𝑊)〉) |
| 8 | | tpeq1 4742 |
. . . . . 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‘𝐾)‘𝑊) |
| 10 | 9 | opeq2i 4877 |
. . . . . . 7
⊢
〈(Base‘ndx), 𝐸〉 = 〈(Base‘ndx),
((TEndo‘𝐾)‘𝑊)〉 |
| 11 | | tpeq1 4742 |
. . . . . . 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‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉}) |
| 12 | 10, 11 | ax-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‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉} |
| 13 | 8, 12 | eqtr4di 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‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉}) |
| 14 | 7, 13 | syl 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‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉}) |
| 15 | 6, 9 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((TEndo‘𝐾)‘𝑤) = 𝐸) |
| 16 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
| 17 | | erngset.t |
. . . . . . . . 9
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 18 | 16, 17 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = 𝑇) |
| 19 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑠‘𝑓) ∘ (𝑡‘𝑓)) = ((𝑠‘𝑓) ∘ (𝑡‘𝑓))) |
| 20 | 18, 19 | mpteq12dv 5233 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))) = (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) |
| 21 | 15, 15, 20 | mpoeq123dv 7508 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))) |
| 22 | 21 | opeq2d 4880 |
. . . . 5
⊢ (𝑤 = 𝑊 → 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉 = 〈(+g‘ndx),
(𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉) |
| 23 | 22 | tpeq2d 4746 |
. . . 4
⊢ (𝑤 = 𝑊 → {〈(Base‘ndx), 𝐸〉,
〈(+g‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉} = {〈(Base‘ndx), 𝐸〉,
〈(+g‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉}) |
| 24 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑠 ∘ 𝑡) = (𝑠 ∘ 𝑡)) |
| 25 | 15, 15, 24 | mpoeq123dv 7508 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡)) = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))) |
| 26 | 25 | opeq2d 4880 |
. . . . 5
⊢ (𝑤 = 𝑊 → 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉 = 〈(.r‘ndx),
(𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))〉) |
| 27 | 26 | tpeq3d 4747 |
. . . 4
⊢ (𝑤 = 𝑊 → {〈(Base‘ndx), 𝐸〉,
〈(+g‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉} = {〈(Base‘ndx), 𝐸〉,
〈(+g‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))〉}) |
| 28 | 14, 23, 27 | 3eqtrd 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 7766 |
. . 3
⊢
{〈(Base‘ndx), 𝐸〉, 〈(+g‘ndx),
(𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))〉} ∈ V |
| 31 | 28, 29, 30 | fvmpt 7016 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈
((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉})‘𝑊) = {〈(Base‘ndx), 𝐸〉,
〈(+g‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))〉}) |
| 32 | 5, 31 | sylan9eq 2797 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐷 = {〈(Base‘ndx), 𝐸〉,
〈(+g‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx),
(𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))〉}) |