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

Definition df-hgmap 40750
Description: Define 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.)
Assertion
Ref Expression
df-hgmap HGMap = (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {π‘Ž ∣ [((DVecHβ€˜π‘˜)β€˜π‘€) / 𝑒][(Baseβ€˜(Scalarβ€˜π‘’)) / 𝑏][((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))}))
Distinct variable group:   π‘Ž,𝑏,π‘˜,π‘š,𝑒,𝑣,𝑀,π‘₯,𝑦

Detailed syntax breakdown of Definition df-hgmap
StepHypRef Expression
1 chg 40749 . 2 class HGMap
2 vk . . 3 setvar π‘˜
3 cvv 3474 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1540 . . . . 5 class π‘˜
6 clh 38850 . . . . 5 class LHyp
75, 6cfv 6543 . . . 4 class (LHypβ€˜π‘˜)
8 va . . . . . . . . . 10 setvar π‘Ž
98cv 1540 . . . . . . . . 9 class π‘Ž
10 vx . . . . . . . . . 10 setvar π‘₯
11 vb . . . . . . . . . . 11 setvar 𝑏
1211cv 1540 . . . . . . . . . 10 class 𝑏
1310cv 1540 . . . . . . . . . . . . . . 15 class π‘₯
14 vv . . . . . . . . . . . . . . . 16 setvar 𝑣
1514cv 1540 . . . . . . . . . . . . . . 15 class 𝑣
16 vu . . . . . . . . . . . . . . . . 17 setvar 𝑒
1716cv 1540 . . . . . . . . . . . . . . . 16 class 𝑒
18 cvsca 17200 . . . . . . . . . . . . . . . 16 class ·𝑠
1917, 18cfv 6543 . . . . . . . . . . . . . . 15 class ( ·𝑠 β€˜π‘’)
2013, 15, 19co 7408 . . . . . . . . . . . . . 14 class (π‘₯( ·𝑠 β€˜π‘’)𝑣)
21 vm . . . . . . . . . . . . . . 15 setvar π‘š
2221cv 1540 . . . . . . . . . . . . . 14 class π‘š
2320, 22cfv 6543 . . . . . . . . . . . . 13 class (π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣))
24 vy . . . . . . . . . . . . . . 15 setvar 𝑦
2524cv 1540 . . . . . . . . . . . . . 14 class 𝑦
2615, 22cfv 6543 . . . . . . . . . . . . . 14 class (π‘šβ€˜π‘£)
274cv 1540 . . . . . . . . . . . . . . . 16 class 𝑀
28 clcd 40452 . . . . . . . . . . . . . . . . 17 class LCDual
295, 28cfv 6543 . . . . . . . . . . . . . . . 16 class (LCDualβ€˜π‘˜)
3027, 29cfv 6543 . . . . . . . . . . . . . . 15 class ((LCDualβ€˜π‘˜)β€˜π‘€)
3130, 18cfv 6543 . . . . . . . . . . . . . 14 class ( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))
3225, 26, 31co 7408 . . . . . . . . . . . . 13 class (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))
3323, 32wceq 1541 . . . . . . . . . . . 12 wff (π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))
34 cbs 17143 . . . . . . . . . . . . 13 class Base
3517, 34cfv 6543 . . . . . . . . . . . 12 class (Baseβ€˜π‘’)
3633, 14, 35wral 3061 . . . . . . . . . . 11 wff βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))
3736, 24, 12crio 7363 . . . . . . . . . 10 class (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£)))
3810, 12, 37cmpt 5231 . . . . . . . . 9 class (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))
399, 38wcel 2106 . . . . . . . 8 wff π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))
40 chdma 40658 . . . . . . . . . 10 class HDMap
415, 40cfv 6543 . . . . . . . . 9 class (HDMapβ€˜π‘˜)
4227, 41cfv 6543 . . . . . . . 8 class ((HDMapβ€˜π‘˜)β€˜π‘€)
4339, 21, 42wsbc 3777 . . . . . . 7 wff [((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))
44 csca 17199 . . . . . . . . 9 class Scalar
4517, 44cfv 6543 . . . . . . . 8 class (Scalarβ€˜π‘’)
4645, 34cfv 6543 . . . . . . 7 class (Baseβ€˜(Scalarβ€˜π‘’))
4743, 11, 46wsbc 3777 . . . . . 6 wff [(Baseβ€˜(Scalarβ€˜π‘’)) / 𝑏][((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))
48 cdvh 39944 . . . . . . . 8 class DVecH
495, 48cfv 6543 . . . . . . 7 class (DVecHβ€˜π‘˜)
5027, 49cfv 6543 . . . . . 6 class ((DVecHβ€˜π‘˜)β€˜π‘€)
5147, 16, 50wsbc 3777 . . . . 5 wff [((DVecHβ€˜π‘˜)β€˜π‘€) / 𝑒][(Baseβ€˜(Scalarβ€˜π‘’)) / 𝑏][((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))
5251, 8cab 2709 . . . 4 class {π‘Ž ∣ [((DVecHβ€˜π‘˜)β€˜π‘€) / 𝑒][(Baseβ€˜(Scalarβ€˜π‘’)) / 𝑏][((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))}
534, 7, 52cmpt 5231 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {π‘Ž ∣ [((DVecHβ€˜π‘˜)β€˜π‘€) / 𝑒][(Baseβ€˜(Scalarβ€˜π‘’)) / 𝑏][((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))})
542, 3, 53cmpt 5231 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {π‘Ž ∣ [((DVecHβ€˜π‘˜)β€˜π‘€) / 𝑒][(Baseβ€˜(Scalarβ€˜π‘’)) / 𝑏][((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))}))
551, 54wceq 1541 1 wff HGMap = (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {π‘Ž ∣ [((DVecHβ€˜π‘˜)β€˜π‘€) / 𝑒][(Baseβ€˜(Scalarβ€˜π‘’)) / 𝑏][((HDMapβ€˜π‘˜)β€˜π‘€) / π‘š]π‘Ž ∈ (π‘₯ ∈ 𝑏 ↦ (℩𝑦 ∈ 𝑏 βˆ€π‘£ ∈ (Baseβ€˜π‘’)(π‘šβ€˜(π‘₯( ·𝑠 β€˜π‘’)𝑣)) = (𝑦( ·𝑠 β€˜((LCDualβ€˜π‘˜)β€˜π‘€))(π‘šβ€˜π‘£))))}))
Colors of variables: wff setvar class
This definition is referenced by:  hgmapffval  40751
  Copyright terms: Public domain W3C validator