Step | Hyp | Ref
| Expression |
1 | | elex 3426 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | fveq2 6717 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | dvhset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | eqtr4di 2796 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
6 | 5 | fveq1d 6719 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
7 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (TEndo‘𝑘) = (TEndo‘𝐾)) |
8 | 7 | fveq1d 6719 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((TEndo‘𝑘)‘𝑤) = ((TEndo‘𝐾)‘𝑤)) |
9 | 6, 8 | xpeq12d 5582 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) = (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))) |
10 | 9 | opeq2d 4791 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(Base‘ndx),
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))〉 = 〈(Base‘ndx),
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))〉) |
11 | 6 | mpteq1d 5144 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))) |
12 | 11 | opeq2d 4791 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → 〈((1st ‘𝑓) ∘ (1st
‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉 = 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉) |
13 | 9, 9, 12 | mpoeq123dv 7286 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉) = (𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)) |
14 | 13 | opeq2d 4791 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉 =
〈(+g‘ndx), (𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉) |
15 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (EDRing‘𝑘) = (EDRing‘𝐾)) |
16 | 15 | fveq1d 6719 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((EDRing‘𝑘)‘𝑤) = ((EDRing‘𝐾)‘𝑤)) |
17 | 16 | opeq2d 4791 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉 = 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉) |
18 | 10, 14, 17 | tpeq123d 4664 |
. . . . 5
⊢ (𝑘 = 𝐾 → {〈(Base‘ndx),
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} = {〈(Base‘ndx),
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉}) |
19 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉 = 〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉) |
20 | 8, 9, 19 | mpoeq123dv 7286 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)) |
21 | 20 | opeq2d 4791 |
. . . . . 6
⊢ (𝑘 = 𝐾 → 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉 = 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉) |
22 | 21 | sneqd 4553 |
. . . . 5
⊢ (𝑘 = 𝐾 → {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉} = {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}) |
23 | 18, 22 | uneq12d 4078 |
. . . 4
⊢ (𝑘 = 𝐾 → ({〈(Base‘ndx),
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}) =
({〈(Base‘ndx), (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉})) |
24 | 4, 23 | mpteq12dv 5140 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ ({〈(Base‘ndx),
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉})) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}))) |
25 | | df-dvech 38830 |
. . 3
⊢ DVecH =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
({〈(Base‘ndx), (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}))) |
26 | 24, 25, 3 | mptfvmpt 7044 |
. 2
⊢ (𝐾 ∈ V →
(DVecH‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}))) |
27 | 1, 26 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (DVecH‘𝐾) = (𝑤 ∈ 𝐻 ↦ ({〈(Base‘ndx),
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))〉, 〈(+g‘ndx),
(𝑓 ∈
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))〉)〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)〉}))) |