Step | Hyp | Ref
| Expression |
1 | | hvmapval.k |
. 2
⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) |
2 | | hvmapval.m |
. . . 4
⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) |
3 | | hvmapval.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 3 | hvmapffval 39772 |
. . . . 5
⊢ (𝐾 ∈ 𝐴 → (HVMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))) |
5 | 4 | fveq1d 6776 |
. . . 4
⊢ (𝐾 ∈ 𝐴 → ((HVMap‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))‘𝑊)) |
6 | 2, 5 | eqtrid 2790 |
. . 3
⊢ (𝐾 ∈ 𝐴 → 𝑀 = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))‘𝑊)) |
7 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊)) |
8 | | hvmapval.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
9 | 7, 8 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = 𝑈) |
10 | 9 | fveq2d 6778 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = (Base‘𝑈)) |
11 | | hvmapval.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
12 | 10, 11 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = 𝑉) |
13 | 9 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 →
(0g‘((DVecH‘𝐾)‘𝑤)) = (0g‘𝑈)) |
14 | | hvmapval.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑈) |
15 | 13, 14 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 →
(0g‘((DVecH‘𝐾)‘𝑤)) = 0 ) |
16 | 15 | sneqd 4573 |
. . . . . 6
⊢ (𝑤 = 𝑊 →
{(0g‘((DVecH‘𝐾)‘𝑤))} = { 0 }) |
17 | 12, 16 | difeq12d 4058 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) = (𝑉 ∖ { 0 })) |
18 | 9 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Scalar‘((DVecH‘𝐾)‘𝑤)) = (Scalar‘𝑈)) |
19 | | hvmapval.s |
. . . . . . . . . 10
⊢ 𝑆 = (Scalar‘𝑈) |
20 | 18, 19 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Scalar‘((DVecH‘𝐾)‘𝑤)) = 𝑆) |
21 | 20 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 →
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤))) = (Base‘𝑆)) |
22 | | hvmapval.r |
. . . . . . . 8
⊢ 𝑅 = (Base‘𝑆) |
23 | 21, 22 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 →
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤))) = 𝑅) |
24 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = ((ocH‘𝐾)‘𝑊)) |
25 | | hvmapval.o |
. . . . . . . . . 10
⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
26 | 24, 25 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = 𝑂) |
27 | 26 | fveq1d 6776 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘{𝑥}) = (𝑂‘{𝑥})) |
28 | 9 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 →
(+g‘((DVecH‘𝐾)‘𝑤)) = (+g‘𝑈)) |
29 | | hvmapval.p |
. . . . . . . . . . 11
⊢ + =
(+g‘𝑈) |
30 | 28, 29 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 →
(+g‘((DVecH‘𝐾)‘𝑤)) = + ) |
31 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → 𝑡 = 𝑡) |
32 | 9 | fveq2d 6778 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘((DVecH‘𝐾)‘𝑤)) = ( ·𝑠
‘𝑈)) |
33 | | hvmapval.t |
. . . . . . . . . . . 12
⊢ · = (
·𝑠 ‘𝑈) |
34 | 32, 33 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘((DVecH‘𝐾)‘𝑤)) = · ) |
35 | 34 | oveqd 7292 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥) = (𝑗 · 𝑥)) |
36 | 30, 31, 35 | oveq123d 7296 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)) = (𝑡 + (𝑗 · 𝑥))) |
37 | 36 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)) ↔ 𝑣 = (𝑡 + (𝑗 · 𝑥)))) |
38 | 27, 37 | rexeqbidv 3337 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)) ↔ ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))) |
39 | 23, 38 | riotaeqbidv 7235 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))) = (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))) |
40 | 12, 39 | mpteq12dv 5165 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)))) = (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))))) |
41 | 17, 40 | mpteq12dv 5165 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))) = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) |
42 | | eqid 2738 |
. . . 4
⊢ (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)))))) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)))))) |
43 | 11 | fvexi 6788 |
. . . . . 6
⊢ 𝑉 ∈ V |
44 | 43 | difexi 5252 |
. . . . 5
⊢ (𝑉 ∖ { 0 }) ∈
V |
45 | 44 | mptex 7099 |
. . . 4
⊢ (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))))) ∈ V |
46 | 41, 42, 45 | fvmpt 6875 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))‘𝑊) = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) |
47 | 6, 46 | sylan9eq 2798 |
. 2
⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) |
48 | 1, 47 | syl 17 |
1
⊢ (𝜑 → 𝑀 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) |