Step | Hyp | Ref
| Expression |
1 | | hlhilset.l |
. 2
⊢ 𝐿 = ((HLHil‘𝐾)‘𝑊) |
2 | | hlhilset.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
3 | | elex 3185 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ V) |
4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐾 ∈ V) |
5 | 2, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ V) |
6 | | hlhilset.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
7 | | fvex 6113 |
. . . . . 6
⊢
(LHyp‘𝐾)
∈ V |
8 | 6, 7 | eqeltri 2684 |
. . . . 5
⊢ 𝐻 ∈ V |
9 | 8 | mptex 6390 |
. . . 4
⊢ (𝑤 ∈ 𝐻 ↦ ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉})) ∈ V |
10 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑘𝐾 |
11 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑘𝐻 |
12 | | nfcsb1v 3515 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}) |
13 | 11, 12 | nfmpt 4674 |
. . . . 5
⊢
Ⅎ𝑘(𝑤 ∈ 𝐻 ↦ ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉})) |
14 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
15 | 14, 6 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
16 | | csbeq1a 3508 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet 〈(*𝑟‘ndx),
((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}) = ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉})) |
17 | 15, 16 | mpteq12dv 4663 |
. . . . 5
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet 〈(*𝑟‘ndx),
((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉})) = (𝑤 ∈ 𝐻 ↦ ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}))) |
18 | | df-hlhil 36243 |
. . . . 5
⊢ HLHil =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet 〈(*𝑟‘ndx),
((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}))) |
19 | 10, 13, 17, 18 | fvmptf 6209 |
. . . 4
⊢ ((𝐾 ∈ V ∧ (𝑤 ∈ 𝐻 ↦ ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉})) ∈ V) → (HLHil‘𝐾) = (𝑤 ∈ 𝐻 ↦ ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}))) |
20 | 5, 9, 19 | sylancl 693 |
. . 3
⊢ (𝜑 → (HLHil‘𝐾) = (𝑤 ∈ 𝐻 ↦ ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}))) |
21 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 = 𝑊) → 𝐾 ∈ V) |
22 | | fvex 6113 |
. . . . . 6
⊢
((DVecH‘𝑘)‘𝑤) ∈ V |
23 | 22 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((DVecH‘𝑘)‘𝑤) ∈ V) |
24 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑢)
∈ V |
25 | 24 | a1i 11 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) → (Base‘𝑢) ∈ V) |
26 | | id 22 |
. . . . . . . . . 10
⊢ (𝑣 = (Base‘𝑢) → 𝑣 = (Base‘𝑢)) |
27 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑢 = ((DVecH‘𝑘)‘𝑤) → 𝑢 = ((DVecH‘𝑘)‘𝑤)) |
28 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (DVecH‘𝑘) = (DVecH‘𝐾)) |
30 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑤 = 𝑊) |
31 | 29, 30 | fveq12d 6109 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((DVecH‘𝑘)‘𝑤) = ((DVecH‘𝐾)‘𝑊)) |
32 | | hlhilset.u |
. . . . . . . . . . . . . 14
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
33 | 31, 32 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((DVecH‘𝑘)‘𝑤) = 𝑈) |
34 | 27, 33 | sylan9eqr 2666 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) → 𝑢 = 𝑈) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) → (Base‘𝑢) = (Base‘𝑈)) |
36 | | hlhilset.v |
. . . . . . . . . . 11
⊢ 𝑉 = (Base‘𝑈) |
37 | 35, 36 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) → (Base‘𝑢) = 𝑉) |
38 | 26, 37 | sylan9eqr 2666 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = 𝑉) |
39 | 38 | opeq2d 4347 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → 〈(Base‘ndx), 𝑣〉 = 〈(Base‘ndx),
𝑉〉) |
40 | 34 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = 𝑈) |
41 | 40 | fveq2d 6107 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → (+g‘𝑢) = (+g‘𝑈)) |
42 | | hlhilset.p |
. . . . . . . . . 10
⊢ + =
(+g‘𝑈) |
43 | 41, 42 | syl6eqr 2662 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → (+g‘𝑢) = + ) |
44 | 43 | opeq2d 4347 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → 〈(+g‘ndx),
(+g‘𝑢)〉 = 〈(+g‘ndx),
+
〉) |
45 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (EDRing‘𝑘) = (EDRing‘𝐾)) |
46 | 45, 30 | fveq12d 6109 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((EDRing‘𝑘)‘𝑤) = ((EDRing‘𝐾)‘𝑊)) |
47 | | hlhilset.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = ((EDRing‘𝐾)‘𝑊) |
48 | 46, 47 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((EDRing‘𝑘)‘𝑤) = 𝐸) |
49 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (HGMap‘𝑘) = (HGMap‘𝐾)) |
50 | 49, 30 | fveq12d 6109 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((HGMap‘𝑘)‘𝑤) = ((HGMap‘𝐾)‘𝑊)) |
51 | | hlhilset.g |
. . . . . . . . . . . . . 14
⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊) |
52 | 50, 51 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((HGMap‘𝑘)‘𝑤) = 𝐺) |
53 | 52 | opeq2d 4347 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) →
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉 =
〈(*𝑟‘ndx), 𝐺〉) |
54 | 48, 53 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉) = (𝐸 sSet
〈(*𝑟‘ndx), 𝐺〉)) |
55 | | hlhilset.r |
. . . . . . . . . . 11
⊢ 𝑅 = (𝐸 sSet
〈(*𝑟‘ndx), 𝐺〉) |
56 | 54, 55 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉) = 𝑅) |
57 | 56 | opeq2d 4347 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉 = 〈(Scalar‘ndx),
𝑅〉) |
58 | 57 | ad2antrr 758 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉 = 〈(Scalar‘ndx),
𝑅〉) |
59 | 39, 44, 58 | tpeq123d 4227 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → {〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} = {〈(Base‘ndx),
𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉}) |
60 | 40 | fveq2d 6107 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → (
·𝑠 ‘𝑢) = ( ·𝑠
‘𝑈)) |
61 | | hlhilset.t |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑈) |
62 | 60, 61 | syl6eqr 2662 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → (
·𝑠 ‘𝑢) = · ) |
63 | 62 | opeq2d 4347 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → 〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉 = 〈(
·𝑠 ‘ndx), ·
〉) |
64 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (HDMap‘𝑘) = (HDMap‘𝐾)) |
65 | 64, 30 | fveq12d 6109 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((HDMap‘𝑘)‘𝑤) = ((HDMap‘𝐾)‘𝑊)) |
66 | | hlhilset.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
67 | 65, 66 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((HDMap‘𝑘)‘𝑤) = 𝑆) |
68 | 67 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → ((HDMap‘𝑘)‘𝑤) = 𝑆) |
69 | 68 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → (((HDMap‘𝑘)‘𝑤)‘𝑦) = (𝑆‘𝑦)) |
70 | 69 | fveq1d 6105 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥) = ((𝑆‘𝑦)‘𝑥)) |
71 | 38, 38, 70 | mpt2eq123dv 6615 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥)) = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝑆‘𝑦)‘𝑥))) |
72 | | hlhilset.i |
. . . . . . . . . 10
⊢ , = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝑆‘𝑦)‘𝑥)) |
73 | 71, 72 | syl6eqr 2662 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥)) = , ) |
74 | 73 | opeq2d 4347 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) →
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉 =
〈(·𝑖‘ndx), , 〉) |
75 | 63, 74 | preq12d 4220 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉} = {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉}) |
76 | 59, 75 | uneq12d 3730 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) ∧ 𝑣 = (Base‘𝑢)) → ({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}) = ({〈(Base‘ndx), 𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉})) |
77 | 25, 76 | csbied 3526 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) ∧ 𝑢 = ((DVecH‘𝑘)‘𝑤)) → ⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx),
𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}) = ({〈(Base‘ndx), 𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉})) |
78 | 23, 77 | csbied 3526 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet 〈(*𝑟‘ndx),
((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}) = ({〈(Base‘ndx), 𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉})) |
79 | 21, 78 | csbied 3526 |
. . 3
⊢ ((𝜑 ∧ 𝑤 = 𝑊) → ⦋𝐾 / 𝑘⦌⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({〈(Base‘ndx), 𝑣〉,
〈(+g‘ndx), (+g‘𝑢)〉, 〈(Scalar‘ndx),
(((EDRing‘𝑘)‘𝑤) sSet
〈(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)〉)〉} ∪ {〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑢)〉,
〈(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))〉}) = ({〈(Base‘ndx), 𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉})) |
80 | 2 | simprd 478 |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝐻) |
81 | | tpex 6855 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑉〉, 〈(+g‘ndx),
+ 〉,
〈(Scalar‘ndx), 𝑅〉} ∈ V |
82 | | prex 4836 |
. . . . 5
⊢ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉} ∈
V |
83 | 81, 82 | unex 6854 |
. . . 4
⊢
({〈(Base‘ndx), 𝑉〉, 〈(+g‘ndx),
+ 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉}) ∈
V |
84 | 83 | a1i 11 |
. . 3
⊢ (𝜑 → ({〈(Base‘ndx),
𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉}) ∈
V) |
85 | 20, 79, 80, 84 | fvmptd 6197 |
. 2
⊢ (𝜑 → ((HLHil‘𝐾)‘𝑊) = ({〈(Base‘ndx), 𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉})) |
86 | 1, 85 | syl5eq 2656 |
1
⊢ (𝜑 → 𝐿 = ({〈(Base‘ndx), 𝑉〉,
〈(+g‘ndx), + 〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), · 〉,
〈(·𝑖‘ndx), , 〉})) |