Step | Hyp | Ref
| Expression |
1 | | hvmapval.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | hvmapval.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | hvmapval.o |
. . . 4
⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
4 | | hvmapval.v |
. . . 4
⊢ 𝑉 = (Base‘𝑈) |
5 | | hvmapval.p |
. . . 4
⊢ + =
(+g‘𝑈) |
6 | | hvmapval.t |
. . . 4
⊢ · = (
·𝑠 ‘𝑈) |
7 | | hvmapval.z |
. . . 4
⊢ 0 =
(0g‘𝑈) |
8 | | hvmapval.s |
. . . 4
⊢ 𝑆 = (Scalar‘𝑈) |
9 | | hvmapval.r |
. . . 4
⊢ 𝑅 = (Base‘𝑆) |
10 | | hvmapval.m |
. . . 4
⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) |
11 | | hvmapval.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | hvmapfval 36066 |
. . 3
⊢ (𝜑 → 𝑀 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))) |
13 | 12 | fveq1d 6105 |
. 2
⊢ (𝜑 → (𝑀‘𝑋) = ((𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))‘𝑋)) |
14 | | hvmapval.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
15 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑈)
∈ V |
16 | 4, 15 | eqeltri 2684 |
. . . 4
⊢ 𝑉 ∈ V |
17 | 16 | mptex 6390 |
. . 3
⊢ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋)))) ∈ V |
18 | | sneq 4135 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
19 | 18 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑂‘{𝑥}) = (𝑂‘{𝑋})) |
20 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑗 · 𝑥) = (𝑗 · 𝑋)) |
21 | 20 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑡 + (𝑗 · 𝑥)) = (𝑡 + (𝑗 · 𝑋))) |
22 | 21 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑣 = (𝑡 + (𝑗 · 𝑥)) ↔ 𝑣 = (𝑡 + (𝑗 · 𝑋)))) |
23 | 19, 22 | rexeqbidv 3130 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)) ↔ ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋)))) |
24 | 23 | riotabidv 6513 |
. . . . 5
⊢ (𝑥 = 𝑋 → (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))) = (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋)))) |
25 | 24 | mpteq2dv 4673 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))) = (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋))))) |
26 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))))) = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥))))) |
27 | 25, 26 | fvmptg 6189 |
. . 3
⊢ ((𝑋 ∈ (𝑉 ∖ { 0 }) ∧ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋)))) ∈ V) → ((𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋))))) |
28 | 14, 17, 27 | sylancl 693 |
. 2
⊢ (𝜑 → ((𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑥})𝑣 = (𝑡 + (𝑗 · 𝑥)))))‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋))))) |
29 | 13, 28 | eqtrd 2644 |
1
⊢ (𝜑 → (𝑀‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑗 ∈ 𝑅 ∃𝑡 ∈ (𝑂‘{𝑋})𝑣 = (𝑡 + (𝑗 · 𝑋))))) |