| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hvmapval.k | . 2
⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) | 
| 2 |  | hvmapval.m | . . . 4
⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) | 
| 3 |  | hvmapval.h | . . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) | 
| 4 | 3 | hvmapffval 41761 | . . . . 5
⊢ (𝐾 ∈ 𝐴 → (HVMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))) | 
| 5 | 4 | fveq1d 6907 | . . . 4
⊢ (𝐾 ∈ 𝐴 → ((HVMap‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))‘𝑊)) | 
| 6 | 2, 5 | eqtrid 2788 | . . 3
⊢ (𝐾 ∈ 𝐴 → 𝑀 = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))‘𝑊)) | 
| 7 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊)) | 
| 8 |  | hvmapval.u | . . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | 
| 9 | 7, 8 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = 𝑈) | 
| 10 | 9 | fveq2d 6909 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = (Base‘𝑈)) | 
| 11 |  | hvmapval.v | . . . . . . 7
⊢ 𝑉 = (Base‘𝑈) | 
| 12 | 10, 11 | eqtr4di 2794 | . . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = 𝑉) | 
| 13 | 9 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑤 = 𝑊 →
(0g‘((DVecH‘𝐾)‘𝑤)) = (0g‘𝑈)) | 
| 14 |  | hvmapval.z | . . . . . . . 8
⊢  0 =
(0g‘𝑈) | 
| 15 | 13, 14 | eqtr4di 2794 | . . . . . . 7
⊢ (𝑤 = 𝑊 →
(0g‘((DVecH‘𝐾)‘𝑤)) = 0 ) | 
| 16 | 15 | sneqd 4637 | . . . . . 6
⊢ (𝑤 = 𝑊 →
{(0g‘((DVecH‘𝐾)‘𝑤))} = { 0 }) | 
| 17 | 12, 16 | difeq12d 4126 | . . . . 5
⊢ (𝑤 = 𝑊 → ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) = (𝑉 ∖ { 0 })) | 
| 18 | 9 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Scalar‘((DVecH‘𝐾)‘𝑤)) = (Scalar‘𝑈)) | 
| 19 |  | hvmapval.s | . . . . . . . . . 10
⊢ 𝑆 = (Scalar‘𝑈) | 
| 20 | 18, 19 | eqtr4di 2794 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Scalar‘((DVecH‘𝐾)‘𝑤)) = 𝑆) | 
| 21 | 20 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑤 = 𝑊 →
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤))) = (Base‘𝑆)) | 
| 22 |  | hvmapval.r | . . . . . . . 8
⊢ 𝑅 = (Base‘𝑆) | 
| 23 | 21, 22 | eqtr4di 2794 | . . . . . . 7
⊢ (𝑤 = 𝑊 →
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤))) = 𝑅) | 
| 24 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = ((ocH‘𝐾)‘𝑊)) | 
| 25 |  | hvmapval.o | . . . . . . . . . 10
⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) | 
| 26 | 24, 25 | eqtr4di 2794 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = 𝑂) | 
| 27 | 26 | fveq1d 6907 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘{𝑥}) = (𝑂‘{𝑥})) | 
| 28 | 9 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 →
(+g‘((DVecH‘𝐾)‘𝑤)) = (+g‘𝑈)) | 
| 29 |  | hvmapval.p | . . . . . . . . . . 11
⊢  + =
(+g‘𝑈) | 
| 30 | 28, 29 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 →
(+g‘((DVecH‘𝐾)‘𝑤)) = + ) | 
| 31 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → 𝑡 = 𝑡) | 
| 32 | 9 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘((DVecH‘𝐾)‘𝑤)) = ( ·𝑠
‘𝑈)) | 
| 33 |  | hvmapval.t | . . . . . . . . . . . 12
⊢  · = (
·𝑠 ‘𝑈) | 
| 34 | 32, 33 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘((DVecH‘𝐾)‘𝑤)) = · ) | 
| 35 | 34 | oveqd 7449 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥) = (𝑗 · 𝑥)) | 
| 36 | 30, 31, 35 | oveq123d 7453 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)) = (𝑡 + (𝑗 · 𝑥))) | 
| 37 | 36 | eqeq2d 2747 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)) ↔ 𝑣 = (𝑡 + (𝑗 · 𝑥)))) | 
| 38 | 27, 37 | rexeqbidv 3346 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)) ↔ ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))) | 
| 39 | 23, 38 | riotaeqbidv 7392 | . . . . . 6
⊢ (𝑤 = 𝑊 → (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))) = (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))) | 
| 40 | 12, 39 | mpteq12dv 5232 | . . . . 5
⊢ (𝑤 = 𝑊 → (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥)))) = (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))))) | 
| 41 | 17, 40 | mpteq12dv 5232 | . . . 4
⊢ (𝑤 = 𝑊 → (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))) = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) | 
| 42 |  | eqid 2736 | . . . 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 6919 | . . . . . 6
⊢ 𝑉 ∈ V | 
| 44 | 43 | difexi 5329 | . . . . 5
⊢ (𝑉 ∖ { 0 }) ∈
V | 
| 45 | 44 | mptex 7244 | . . . 4
⊢ (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))))) ∈ V | 
| 46 | 41, 42, 45 | fvmpt 7015 | . . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ ((Base‘((DVecH‘𝐾)‘𝑤)) ∖
{(0g‘((DVecH‘𝐾)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (℩𝑗 ∈
(Base‘(Scalar‘((DVecH‘𝐾)‘𝑤)))∃𝑡 ∈ (((ocH‘𝐾)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝐾)‘𝑤))(𝑗( ·𝑠
‘((DVecH‘𝐾)‘𝑤))𝑥))))))‘𝑊) = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) | 
| 47 | 6, 46 | sylan9eq 2796 | . 2
⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) | 
| 48 | 1, 47 | syl 17 | 1
⊢ (𝜑 → 𝑀 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) |