Step | Hyp | Ref
| Expression |
1 | | elex 3448 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | fveq2 6768 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | dvaset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | eqtr4di 2797 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6768 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
6 | 5 | fveq1d 6770 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
7 | 6 | opeq2d 4816 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(Base‘ndx),
((LTrn‘𝑘)‘𝑤)〉 =
〈(Base‘ndx), ((LTrn‘𝐾)‘𝑤)〉) |
8 | | eqidd 2740 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔)) |
9 | 6, 6, 8 | mpoeq123dv 7341 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))) |
10 | 9 | opeq2d 4816 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉) |
11 | | fveq2 6768 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (EDRing‘𝑘) = (EDRing‘𝐾)) |
12 | 11 | fveq1d 6770 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((EDRing‘𝑘)‘𝑤) = ((EDRing‘𝐾)‘𝑤)) |
13 | 12 | opeq2d 4816 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉 = 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉) |
14 | 7, 10, 13 | tpeq123d 4689 |
. . . . 5
⊢ (𝑘 = 𝐾 → {〈(Base‘ndx),
((LTrn‘𝑘)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉}) |
15 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (TEndo‘𝑘) = (TEndo‘𝐾)) |
16 | 15 | fveq1d 6770 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((TEndo‘𝑘)‘𝑤) = ((TEndo‘𝐾)‘𝑤)) |
17 | | eqidd 2740 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑠‘𝑓) = (𝑠‘𝑓)) |
18 | 16, 6, 17 | mpoeq123dv 7341 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))) |
19 | 18 | opeq2d 4816 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉 = 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉) |
20 | 19 | sneqd 4578 |
. . . . 5
⊢ (𝑘 = 𝐾 → {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉} = {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}) |
21 | 14, 20 | uneq12d 4102 |
. . . 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 5169 |
. . 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 38996 |
. . 3
⊢ DVecA =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
({〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |
24 | 22, 23, 3 | mptfvmpt 7098 |
. 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‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |