Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | fveq2 6839 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | dvhset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6839 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
6 | 5 | fveq1d 6841 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
7 | | fveq2 6839 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (TEndo‘𝑘) = (TEndo‘𝐾)) |
8 | 7 | fveq1d 6841 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((TEndo‘𝑘)‘𝑤) = ((TEndo‘𝐾)‘𝑤)) |
9 | 6, 8 | xpeq12d 5662 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) = (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))) |
10 | 9 | opeq2d 4835 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ⟨(Base‘ndx),
(((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤))⟩ = ⟨(Base‘ndx),
(((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤))⟩) |
11 | 6 | mpteq1d 5198 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))) |
12 | 11 | opeq2d 4835 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ⟨((1st ‘𝑓) ∘ (1st
‘𝑔)), (ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩ = ⟨((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩) |
13 | 9, 9, 12 | mpoeq123dv 7426 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)), 𝑔 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝑘)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩) = (𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)), 𝑔 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ ⟨((1st
‘𝑓) ∘
(1st ‘𝑔)),
(ℎ ∈ ((LTrn‘𝐾)‘𝑤) ↦ (((2nd ‘𝑓)‘ℎ) ∘ ((2nd ‘𝑔)‘ℎ)))⟩)) |
14 | 13 | opeq2d 4835 |
. . . . . 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 6839 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (EDRing‘𝑘) = (EDRing‘𝐾)) |
16 | 15 | fveq1d 6841 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((EDRing‘𝑘)‘𝑤) = ((EDRing‘𝐾)‘𝑤)) |
17 | 16 | opeq2d 4835 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ⟨(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)⟩ = ⟨(Scalar‘ndx),
((EDRing‘𝐾)‘𝑤)⟩) |
18 | 10, 14, 17 | tpeq123d 4707 |
. . . . 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 7426 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)) |
21 | 20 | opeq2d 4835 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ⟨(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)⟩ = ⟨(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)⟩) |
22 | 21 | sneqd 4596 |
. . . . 5
⊢ (𝑘 = 𝐾 → {⟨(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ (((LTrn‘𝑘)‘𝑤) × ((TEndo‘𝑘)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)⟩} = {⟨(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑓 ∈ (((LTrn‘𝐾)‘𝑤) × ((TEndo‘𝐾)‘𝑤)) ↦ ⟨(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))⟩)⟩}) |
23 | 18, 22 | uneq12d 4122 |
. . . 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 5194 |
. . 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 39480 |
. . 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 7174 |
. 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 ‘𝑓))⟩)⟩}))) |