| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
| 2 | | fveq2 6906 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
| 3 | | dvaset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
| 5 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
| 6 | 5 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
| 7 | 6 | opeq2d 4880 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(Base‘ndx),
((LTrn‘𝑘)‘𝑤)〉 =
〈(Base‘ndx), ((LTrn‘𝐾)‘𝑤)〉) |
| 8 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔)) |
| 9 | 6, 6, 8 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))) |
| 10 | 9 | opeq2d 4880 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉) |
| 11 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (EDRing‘𝑘) = (EDRing‘𝐾)) |
| 12 | 11 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((EDRing‘𝑘)‘𝑤) = ((EDRing‘𝐾)‘𝑤)) |
| 13 | 12 | opeq2d 4880 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉 = 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉) |
| 14 | 7, 10, 13 | tpeq123d 4748 |
. . . . 5
⊢ (𝑘 = 𝐾 → {〈(Base‘ndx),
((LTrn‘𝑘)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉}) |
| 15 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (TEndo‘𝑘) = (TEndo‘𝐾)) |
| 16 | 15 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((TEndo‘𝑘)‘𝑤) = ((TEndo‘𝐾)‘𝑤)) |
| 17 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑠‘𝑓) = (𝑠‘𝑓)) |
| 18 | 16, 6, 17 | mpoeq123dv 7508 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))) |
| 19 | 18 | opeq2d 4880 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉 = 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉) |
| 20 | 19 | sneqd 4638 |
. . . . 5
⊢ (𝑘 = 𝐾 → {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉} = {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}) |
| 21 | 14, 20 | uneq12d 4169 |
. . . 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‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉})) |
| 22 | 4, 21 | mpteq12dv 5233 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ ({〈(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‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |
| 23 | | df-dveca 41005 |
. . 3
⊢ DVecA =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
({〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |
| 24 | 22, 23, 3 | mptfvmpt 7248 |
. 2
⊢ (𝐾 ∈ V →
(DVecA‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |
| 25 | 1, 24 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (DVecA‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |