Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hgmapfval Structured version   Visualization version   GIF version

Theorem hgmapfval 37698
Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
Hypotheses
Ref Expression
hgmapval.h 𝐻 = (LHyp‘𝐾)
hgmapfval.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
hgmapfval.v 𝑉 = (Base‘𝑈)
hgmapfval.t · = ( ·𝑠𝑈)
hgmapfval.r 𝑅 = (Scalar‘𝑈)
hgmapfval.b 𝐵 = (Base‘𝑅)
hgmapfval.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
hgmapfval.s = ( ·𝑠𝐶)
hgmapfval.m 𝑀 = ((HDMap‘𝐾)‘𝑊)
hgmapfval.i 𝐼 = ((HGMap‘𝐾)‘𝑊)
hgmapfval.k (𝜑 → (𝐾𝑌𝑊𝐻))
Assertion
Ref Expression
hgmapfval (𝜑𝐼 = (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))))
Distinct variable groups:   𝑥,𝑣,𝑦,𝐾   𝑣,𝐵,𝑥,𝑦   𝑣,𝑀,𝑥,𝑦   𝑣,𝑈,𝑥,𝑦   𝑣,𝑉   𝑣,𝑊,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑣)   𝐶(𝑥,𝑦,𝑣)   𝑅(𝑥,𝑦,𝑣)   (𝑥,𝑦,𝑣)   · (𝑥,𝑦,𝑣)   𝐻(𝑥,𝑦,𝑣)   𝐼(𝑥,𝑦,𝑣)   𝑉(𝑥,𝑦)   𝑌(𝑥,𝑦,𝑣)

Proof of Theorem hgmapfval
Dummy variables 𝑤 𝑎 𝑏 𝑚 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hgmapfval.k . 2 (𝜑 → (𝐾𝑌𝑊𝐻))
2 hgmapfval.i . . . 4 𝐼 = ((HGMap‘𝐾)‘𝑊)
3 hgmapval.h . . . . . 6 𝐻 = (LHyp‘𝐾)
43hgmapffval 37697 . . . . 5 (𝐾𝑌 → (HGMap‘𝐾) = (𝑤𝐻 ↦ {𝑎[((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))))}))
54fveq1d 6355 . . . 4 (𝐾𝑌 → ((HGMap‘𝐾)‘𝑊) = ((𝑤𝐻 ↦ {𝑎[((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))))})‘𝑊))
62, 5syl5eq 2806 . . 3 (𝐾𝑌𝐼 = ((𝑤𝐻 ↦ {𝑎[((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))))})‘𝑊))
7 fveq2 6353 . . . . . . . 8 (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
8 hgmapfval.u . . . . . . . 8 𝑈 = ((DVecH‘𝐾)‘𝑊)
97, 8syl6eqr 2812 . . . . . . 7 (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = 𝑈)
10 fveq2 6353 . . . . . . . . . 10 (𝑤 = 𝑊 → ((HDMap‘𝐾)‘𝑤) = ((HDMap‘𝐾)‘𝑊))
11 hgmapfval.m . . . . . . . . . 10 𝑀 = ((HDMap‘𝐾)‘𝑊)
1210, 11syl6eqr 2812 . . . . . . . . 9 (𝑤 = 𝑊 → ((HDMap‘𝐾)‘𝑤) = 𝑀)
13 fveq2 6353 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑊 → ((LCDual‘𝐾)‘𝑤) = ((LCDual‘𝐾)‘𝑊))
1413fveq2d 6357 . . . . . . . . . . . . . . 15 (𝑤 = 𝑊 → ( ·𝑠 ‘((LCDual‘𝐾)‘𝑤)) = ( ·𝑠 ‘((LCDual‘𝐾)‘𝑊)))
1514oveqd 6831 . . . . . . . . . . . . . 14 (𝑤 = 𝑊 → (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)))
1615eqeq2d 2770 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → ((𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)) ↔ (𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))))
1716ralbidv 3124 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)) ↔ ∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))))
1817riotabidv 6777 . . . . . . . . . . 11 (𝑤 = 𝑊 → (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))) = (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))))
1918mpteq2dv 4897 . . . . . . . . . 10 (𝑤 = 𝑊 → (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)))) = (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)))))
2019eleq2d 2825 . . . . . . . . 9 (𝑤 = 𝑊 → (𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)))) ↔ 𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))))))
2112, 20sbceqbid 3583 . . . . . . . 8 (𝑤 = 𝑊 → ([((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)))) ↔ [𝑀 / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))))))
2221sbcbidv 3631 . . . . . . 7 (𝑤 = 𝑊 → ([(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)))) ↔ [(Base‘(Scalar‘𝑢)) / 𝑏][𝑀 / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))))))
239, 22sbceqbid 3583 . . . . . 6 (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)))) ↔ [𝑈 / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][𝑀 / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))))))
24 fvex 6363 . . . . . . . 8 ((DVecH‘𝐾)‘𝑊) ∈ V
258, 24eqeltri 2835 . . . . . . 7 𝑈 ∈ V
26 fvex 6363 . . . . . . 7 (Base‘(Scalar‘𝑢)) ∈ V
27 fvex 6363 . . . . . . . 8 ((HDMap‘𝐾)‘𝑊) ∈ V
2811, 27eqeltri 2835 . . . . . . 7 𝑀 ∈ V
29 simp2 1132 . . . . . . . . . 10 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → 𝑏 = (Base‘(Scalar‘𝑢)))
30 simp1 1131 . . . . . . . . . . . . 13 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → 𝑢 = 𝑈)
3130fveq2d 6357 . . . . . . . . . . . 12 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → (Scalar‘𝑢) = (Scalar‘𝑈))
32 hgmapfval.r . . . . . . . . . . . 12 𝑅 = (Scalar‘𝑈)
3331, 32syl6eqr 2812 . . . . . . . . . . 11 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → (Scalar‘𝑢) = 𝑅)
3433fveq2d 6357 . . . . . . . . . 10 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → (Base‘(Scalar‘𝑢)) = (Base‘𝑅))
3529, 34eqtrd 2794 . . . . . . . . 9 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → 𝑏 = (Base‘𝑅))
36 hgmapfval.b . . . . . . . . 9 𝐵 = (Base‘𝑅)
3735, 36syl6eqr 2812 . . . . . . . 8 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → 𝑏 = 𝐵)
38 simp2 1132 . . . . . . . . . 10 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → 𝑏 = 𝐵)
39 simp1 1131 . . . . . . . . . . . . . 14 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → 𝑢 = 𝑈)
4039fveq2d 6357 . . . . . . . . . . . . 13 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (Base‘𝑢) = (Base‘𝑈))
41 hgmapfval.v . . . . . . . . . . . . 13 𝑉 = (Base‘𝑈)
4240, 41syl6eqr 2812 . . . . . . . . . . . 12 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (Base‘𝑢) = 𝑉)
43 simp3 1133 . . . . . . . . . . . . . 14 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → 𝑚 = 𝑀)
4439fveq2d 6357 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → ( ·𝑠𝑢) = ( ·𝑠𝑈))
45 hgmapfval.t . . . . . . . . . . . . . . . 16 · = ( ·𝑠𝑈)
4644, 45syl6eqr 2812 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → ( ·𝑠𝑢) = · )
4746oveqd 6831 . . . . . . . . . . . . . 14 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (𝑥( ·𝑠𝑢)𝑣) = (𝑥 · 𝑣))
4843, 47fveq12d 6359 . . . . . . . . . . . . 13 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑀‘(𝑥 · 𝑣)))
49 eqidd 2761 . . . . . . . . . . . . . . . . 17 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → ((LCDual‘𝐾)‘𝑊) = ((LCDual‘𝐾)‘𝑊))
50 hgmapfval.c . . . . . . . . . . . . . . . . 17 𝐶 = ((LCDual‘𝐾)‘𝑊)
5149, 50syl6eqr 2812 . . . . . . . . . . . . . . . 16 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → ((LCDual‘𝐾)‘𝑊) = 𝐶)
5251fveq2d 6357 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → ( ·𝑠 ‘((LCDual‘𝐾)‘𝑊)) = ( ·𝑠𝐶))
53 hgmapfval.s . . . . . . . . . . . . . . 15 = ( ·𝑠𝐶)
5452, 53syl6eqr 2812 . . . . . . . . . . . . . 14 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → ( ·𝑠 ‘((LCDual‘𝐾)‘𝑊)) = )
55 eqidd 2761 . . . . . . . . . . . . . 14 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → 𝑦 = 𝑦)
5643fveq1d 6355 . . . . . . . . . . . . . 14 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (𝑚𝑣) = (𝑀𝑣))
5754, 55, 56oveq123d 6835 . . . . . . . . . . . . 13 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)) = (𝑦 (𝑀𝑣)))
5848, 57eqeq12d 2775 . . . . . . . . . . . 12 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → ((𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)) ↔ (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣))))
5942, 58raleqbidv 3291 . . . . . . . . . . 11 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (∀𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)) ↔ ∀𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣))))
6038, 59riotaeqbidv 6778 . . . . . . . . . 10 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣))) = (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣))))
6138, 60mpteq12dv 4885 . . . . . . . . 9 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)))) = (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))))
6261eleq2d 2825 . . . . . . . 8 ((𝑢 = 𝑈𝑏 = 𝐵𝑚 = 𝑀) → (𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)))) ↔ 𝑎 ∈ (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣))))))
6337, 62syld3an2 1519 . . . . . . 7 ((𝑢 = 𝑈𝑏 = (Base‘(Scalar‘𝑢)) ∧ 𝑚 = 𝑀) → (𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)))) ↔ 𝑎 ∈ (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣))))))
6425, 26, 28, 63sbc3ie 3648 . . . . . 6 ([𝑈 / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][𝑀 / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(𝑚𝑣)))) ↔ 𝑎 ∈ (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))))
6523, 64syl6bb 276 . . . . 5 (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣)))) ↔ 𝑎 ∈ (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣))))))
6665abbi1dv 2881 . . . 4 (𝑤 = 𝑊 → {𝑎[((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))))} = (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))))
67 eqid 2760 . . . 4 (𝑤𝐻 ↦ {𝑎[((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))))}) = (𝑤𝐻 ↦ {𝑎[((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))))})
68 fvex 6363 . . . . . 6 (Base‘𝑅) ∈ V
6936, 68eqeltri 2835 . . . . 5 𝐵 ∈ V
7069mptex 6651 . . . 4 (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))) ∈ V
7166, 67, 70fvmpt 6445 . . 3 (𝑊𝐻 → ((𝑤𝐻 ↦ {𝑎[((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝐾)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝐾)‘𝑤))(𝑚𝑣))))})‘𝑊) = (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))))
726, 71sylan9eq 2814 . 2 ((𝐾𝑌𝑊𝐻) → 𝐼 = (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))))
731, 72syl 17 1 (𝜑𝐼 = (𝑥𝐵 ↦ (𝑦𝐵𝑣𝑉 (𝑀‘(𝑥 · 𝑣)) = (𝑦 (𝑀𝑣)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  {cab 2746  wral 3050  Vcvv 3340  [wsbc 3576  cmpt 4881  cfv 6049  crio 6774  (class class class)co 6814  Basecbs 16079  Scalarcsca 16166   ·𝑠 cvsca 16167  LHypclh 35791  DVecHcdvh 36887  LCDualclcd 37395  HDMapchdma 37602  HGMapchg 37695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-hgmap 37696
This theorem is referenced by:  hgmapval  37699  hgmapfnN  37700
  Copyright terms: Public domain W3C validator