Step | Hyp | Ref
| Expression |
1 | | dvaset.u |
. 2
⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) |
2 | | dvaset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
3 | 2 | dvafset 39018 |
. . . 4
⊢ (𝐾 ∈ 𝑋 → (DVecA‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |
4 | 3 | fveq1d 6776 |
. . 3
⊢ (𝐾 ∈ 𝑋 → ((DVecA‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}))‘𝑊)) |
5 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
6 | | dvaset.t |
. . . . . . . 8
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
7 | 5, 6 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = 𝑇) |
8 | 7 | opeq2d 4811 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉 =
〈(Base‘ndx), 𝑇〉) |
9 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔)) |
10 | 7, 7, 9 | mpoeq123dv 7350 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))) |
11 | 10 | opeq2d 4811 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
(𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉) |
12 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((EDRing‘𝐾)‘𝑤) = ((EDRing‘𝐾)‘𝑊)) |
13 | | dvaset.d |
. . . . . . . 8
⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) |
14 | 12, 13 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((EDRing‘𝐾)‘𝑤) = 𝐷) |
15 | 14 | opeq2d 4811 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉 = 〈(Scalar‘ndx), 𝐷〉) |
16 | 8, 11, 15 | tpeq123d 4684 |
. . . . 5
⊢ (𝑤 = 𝑊 → {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} = {〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉}) |
17 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((TEndo‘𝐾)‘𝑤) = ((TEndo‘𝐾)‘𝑊)) |
18 | | dvaset.e |
. . . . . . . . 9
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
19 | 17, 18 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((TEndo‘𝐾)‘𝑤) = 𝐸) |
20 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑠‘𝑓) = (𝑠‘𝑓)) |
21 | 19, 7, 20 | mpoeq123dv 7350 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓)) = (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))) |
22 | 21 | opeq2d 4811 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉 = 〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉) |
23 | 22 | sneqd 4573 |
. . . . 5
⊢ (𝑤 = 𝑊 → {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉} = {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉}) |
24 | 16, 23 | uneq12d 4098 |
. . . 4
⊢ (𝑤 = 𝑊 → ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑠‘𝑓))〉}) = ({〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉})) |
25 | | eqid 2738 |
. . . 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 7597 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑇〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∈
V |
27 | | snex 5354 |
. . . . 5
⊢ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉} ∈ V |
28 | 26, 27 | unex 7596 |
. . . 4
⊢
({〈(Base‘ndx), 𝑇〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉}) ∈ V |
29 | 24, 25, 28 | fvmpt 6875 |
. . 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 2798 |
. 2
⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ((DVecA‘𝐾)‘𝑊) = ({〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉})) |
31 | 1, 30 | eqtrid 2790 |
1
⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑈 = ({〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx), 𝐷〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ 𝐸, 𝑓 ∈ 𝑇 ↦ (𝑠‘𝑓))〉})) |