| Step | Hyp | Ref
| Expression |
| 1 | | dvaset.u |
. 2
⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) |
| 2 | | dvaset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 3 | 2 | dvafset 41006 |
. . . 4
⊢ (𝐾 ∈ 𝑋 → (DVecA‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |
| 4 | 3 | fveq1d 6908 |
. . 3
⊢ (𝐾 ∈ 𝑋 → ((DVecA‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))‘𝑊)) |
| 5 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
| 6 | | dvaset.t |
. . . . . . . 8
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = 𝑇) |
| 8 | 7 | opeq2d 4880 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉 =
〈(Base‘ndx), 𝑇〉) |
| 9 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔)) |
| 10 | 7, 7, 9 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))) |
| 11 | 10 | opeq2d 4880 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
(𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉) |
| 12 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((EDRing‘𝐾)‘𝑤) = ((EDRing‘𝐾)‘𝑊)) |
| 13 | | dvaset.d |
. . . . . . . 8
⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((EDRing‘𝐾)‘𝑤) = 𝐷) |
| 15 | 14 | opeq2d 4880 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉 = 〈(Scalar‘ndx), 𝐷〉) |
| 16 | 8, 11, 15 | tpeq123d 4748 |
. . . . 5
⊢ (𝑤 = 𝑊 → {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} = {〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉}) |
| 17 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((TEndo‘𝐾)‘𝑤) = ((TEndo‘𝐾)‘𝑊)) |
| 18 | | dvaset.e |
. . . . . . . . 9
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
| 19 | 17, 18 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((TEndo‘𝐾)‘𝑤) = 𝐸) |
| 20 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑠‘𝑓) = (𝑠‘𝑓)) |
| 21 | 19, 7, 20 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓)) = (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))) |
| 22 | 21 | opeq2d 4880 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉 = 〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉) |
| 23 | 22 | sneqd 4638 |
. . . . 5
⊢ (𝑤 = 𝑊 → {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉} = {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉}) |
| 24 | 16, 23 | uneq12d 4169 |
. . . 4
⊢ (𝑤 = 𝑊 → ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}) = ({〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉})) |
| 25 | | eqid 2737 |
. . . 4
⊢ (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉})) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉})) |
| 26 | | tpex 7766 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑇〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∈
V |
| 27 | | snex 5436 |
. . . . 5
⊢ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉} ∈ V |
| 28 | 26, 27 | unex 7764 |
. . . 4
⊢
({〈(Base‘ndx), 𝑇〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉}) ∈ V |
| 29 | 24, 25, 28 | fvmpt 7016 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))‘𝑊) = ({〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉})) |
| 30 | 4, 29 | sylan9eq 2797 |
. 2
⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ((DVecA‘𝐾)‘𝑊) = ({〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉})) |
| 31 | 1, 30 | eqtrid 2789 |
1
⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑈 = ({〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉})) |