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

Theorem hgmapmul 37909
Description: Part 15 of [Baer] p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015.)
Hypotheses
Ref Expression
hgmapmul.h 𝐻 = (LHyp‘𝐾)
hgmapmul.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
hgmapmul.r 𝑅 = (Scalar‘𝑈)
hgmapmul.b 𝐵 = (Base‘𝑅)
hgmapmul.t · = (.r𝑅)
hgmapmul.g 𝐺 = ((HGMap‘𝐾)‘𝑊)
hgmapmul.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
hgmapmul.x (𝜑𝑋𝐵)
hgmapmul.y (𝜑𝑌𝐵)
Assertion
Ref Expression
hgmapmul (𝜑 → (𝐺‘(𝑋 · 𝑌)) = ((𝐺𝑌) · (𝐺𝑋)))

Proof of Theorem hgmapmul
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 hgmapmul.h . . . 4 𝐻 = (LHyp‘𝐾)
2 hgmapmul.u . . . 4 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 eqid 2798 . . . 4 (Base‘𝑈) = (Base‘𝑈)
4 eqid 2798 . . . 4 (0g𝑈) = (0g𝑈)
5 hgmapmul.k . . . 4 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
61, 2, 3, 4, 5dvh1dim 37456 . . 3 (𝜑 → ∃𝑡 ∈ (Base‘𝑈)𝑡 ≠ (0g𝑈))
7 eqid 2798 . . . . . . . . 9 ((LCDual‘𝐾)‘𝑊) = ((LCDual‘𝐾)‘𝑊)
81, 7, 5lcdlmod 37606 . . . . . . . 8 (𝜑 → ((LCDual‘𝐾)‘𝑊) ∈ LMod)
983ad2ant1 1164 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((LCDual‘𝐾)‘𝑊) ∈ LMod)
10 hgmapmul.r . . . . . . . . 9 𝑅 = (Scalar‘𝑈)
11 hgmapmul.b . . . . . . . . 9 𝐵 = (Base‘𝑅)
12 eqid 2798 . . . . . . . . 9 (Scalar‘((LCDual‘𝐾)‘𝑊)) = (Scalar‘((LCDual‘𝐾)‘𝑊))
13 eqid 2798 . . . . . . . . 9 (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))) = (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊)))
14 hgmapmul.g . . . . . . . . 9 𝐺 = ((HGMap‘𝐾)‘𝑊)
15 hgmapmul.x . . . . . . . . 9 (𝜑𝑋𝐵)
161, 2, 10, 11, 7, 12, 13, 14, 5, 15hgmapdcl 37904 . . . . . . . 8 (𝜑 → (𝐺𝑋) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
17163ad2ant1 1164 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (𝐺𝑋) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
18 hgmapmul.y . . . . . . . . 9 (𝜑𝑌𝐵)
191, 2, 10, 11, 7, 12, 13, 14, 5, 18hgmapdcl 37904 . . . . . . . 8 (𝜑 → (𝐺𝑌) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
20193ad2ant1 1164 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (𝐺𝑌) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
21 eqid 2798 . . . . . . . 8 (Base‘((LCDual‘𝐾)‘𝑊)) = (Base‘((LCDual‘𝐾)‘𝑊))
22 eqid 2798 . . . . . . . 8 ((HDMap‘𝐾)‘𝑊) = ((HDMap‘𝐾)‘𝑊)
2353ad2ant1 1164 . . . . . . . 8 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
24 simp2 1168 . . . . . . . 8 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → 𝑡 ∈ (Base‘𝑈))
251, 2, 3, 7, 21, 22, 23, 24hdmapcl 37844 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((HDMap‘𝐾)‘𝑊)‘𝑡) ∈ (Base‘((LCDual‘𝐾)‘𝑊)))
26 eqid 2798 . . . . . . . 8 ( ·𝑠 ‘((LCDual‘𝐾)‘𝑊)) = ( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))
27 eqid 2798 . . . . . . . 8 (.r‘(Scalar‘((LCDual‘𝐾)‘𝑊))) = (.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))
2821, 12, 26, 13, 27lmodvsass 19203 . . . . . . 7 ((((LCDual‘𝐾)‘𝑊) ∈ LMod ∧ ((𝐺𝑋) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))) ∧ (𝐺𝑌) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))) ∧ (((HDMap‘𝐾)‘𝑊)‘𝑡) ∈ (Base‘((LCDual‘𝐾)‘𝑊)))) → (((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌))( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)) = ((𝐺𝑋)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))((𝐺𝑌)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡))))
299, 17, 20, 25, 28syl13anc 1492 . . . . . 6 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌))( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)) = ((𝐺𝑋)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))((𝐺𝑌)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡))))
301, 2, 5dvhlmod 37124 . . . . . . . . . 10 (𝜑𝑈 ∈ LMod)
31303ad2ant1 1164 . . . . . . . . 9 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → 𝑈 ∈ LMod)
32153ad2ant1 1164 . . . . . . . . 9 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → 𝑋𝐵)
33183ad2ant1 1164 . . . . . . . . 9 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → 𝑌𝐵)
34 eqid 2798 . . . . . . . . . 10 ( ·𝑠𝑈) = ( ·𝑠𝑈)
35 hgmapmul.t . . . . . . . . . 10 · = (.r𝑅)
363, 10, 34, 11, 35lmodvsass 19203 . . . . . . . . 9 ((𝑈 ∈ LMod ∧ (𝑋𝐵𝑌𝐵𝑡 ∈ (Base‘𝑈))) → ((𝑋 · 𝑌)( ·𝑠𝑈)𝑡) = (𝑋( ·𝑠𝑈)(𝑌( ·𝑠𝑈)𝑡)))
3731, 32, 33, 24, 36syl13anc 1492 . . . . . . . 8 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((𝑋 · 𝑌)( ·𝑠𝑈)𝑡) = (𝑋( ·𝑠𝑈)(𝑌( ·𝑠𝑈)𝑡)))
3837fveq2d 6414 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((HDMap‘𝐾)‘𝑊)‘((𝑋 · 𝑌)( ·𝑠𝑈)𝑡)) = (((HDMap‘𝐾)‘𝑊)‘(𝑋( ·𝑠𝑈)(𝑌( ·𝑠𝑈)𝑡))))
393, 10, 34, 11lmodvscl 19195 . . . . . . . . 9 ((𝑈 ∈ LMod ∧ 𝑌𝐵𝑡 ∈ (Base‘𝑈)) → (𝑌( ·𝑠𝑈)𝑡) ∈ (Base‘𝑈))
4031, 33, 24, 39syl3anc 1491 . . . . . . . 8 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (𝑌( ·𝑠𝑈)𝑡) ∈ (Base‘𝑈))
411, 2, 3, 34, 10, 11, 7, 26, 22, 14, 23, 40, 32hgmapvs 37905 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((HDMap‘𝐾)‘𝑊)‘(𝑋( ·𝑠𝑈)(𝑌( ·𝑠𝑈)𝑡))) = ((𝐺𝑋)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘(𝑌( ·𝑠𝑈)𝑡))))
421, 2, 3, 34, 10, 11, 7, 26, 22, 14, 23, 24, 33hgmapvs 37905 . . . . . . . 8 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((HDMap‘𝐾)‘𝑊)‘(𝑌( ·𝑠𝑈)𝑡)) = ((𝐺𝑌)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)))
4342oveq2d 6893 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((𝐺𝑋)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘(𝑌( ·𝑠𝑈)𝑡))) = ((𝐺𝑋)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))((𝐺𝑌)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡))))
4438, 41, 433eqtrd 2836 . . . . . 6 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((HDMap‘𝐾)‘𝑊)‘((𝑋 · 𝑌)( ·𝑠𝑈)𝑡)) = ((𝐺𝑋)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))((𝐺𝑌)( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡))))
4510, 11, 35lmodmcl 19190 . . . . . . . . 9 ((𝑈 ∈ LMod ∧ 𝑋𝐵𝑌𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
4630, 15, 18, 45syl3anc 1491 . . . . . . . 8 (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
47463ad2ant1 1164 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (𝑋 · 𝑌) ∈ 𝐵)
481, 2, 3, 34, 10, 11, 7, 26, 22, 14, 23, 24, 47hgmapvs 37905 . . . . . 6 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((HDMap‘𝐾)‘𝑊)‘((𝑋 · 𝑌)( ·𝑠𝑈)𝑡)) = ((𝐺‘(𝑋 · 𝑌))( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)))
4929, 44, 483eqtr2rd 2839 . . . . 5 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((𝐺‘(𝑋 · 𝑌))( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)) = (((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌))( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)))
50 eqid 2798 . . . . . 6 (0g‘((LCDual‘𝐾)‘𝑊)) = (0g‘((LCDual‘𝐾)‘𝑊))
511, 7, 5lcdlvec 37605 . . . . . . 7 (𝜑 → ((LCDual‘𝐾)‘𝑊) ∈ LVec)
52513ad2ant1 1164 . . . . . 6 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((LCDual‘𝐾)‘𝑊) ∈ LVec)
531, 2, 10, 11, 7, 12, 13, 14, 5, 46hgmapdcl 37904 . . . . . . 7 (𝜑 → (𝐺‘(𝑋 · 𝑌)) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
54533ad2ant1 1164 . . . . . 6 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (𝐺‘(𝑋 · 𝑌)) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
5512, 13, 27lmodmcl 19190 . . . . . . . 8 ((((LCDual‘𝐾)‘𝑊) ∈ LMod ∧ (𝐺𝑋) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))) ∧ (𝐺𝑌) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊)))) → ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌)) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
568, 16, 19, 55syl3anc 1491 . . . . . . 7 (𝜑 → ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌)) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
57563ad2ant1 1164 . . . . . 6 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌)) ∈ (Base‘(Scalar‘((LCDual‘𝐾)‘𝑊))))
58 simp3 1169 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → 𝑡 ≠ (0g𝑈))
591, 2, 3, 4, 7, 50, 22, 23, 24hdmapeq0 37858 . . . . . . . 8 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((((HDMap‘𝐾)‘𝑊)‘𝑡) = (0g‘((LCDual‘𝐾)‘𝑊)) ↔ 𝑡 = (0g𝑈)))
6059necon3bid 3014 . . . . . . 7 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → ((((HDMap‘𝐾)‘𝑊)‘𝑡) ≠ (0g‘((LCDual‘𝐾)‘𝑊)) ↔ 𝑡 ≠ (0g𝑈)))
6158, 60mpbird 249 . . . . . 6 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((HDMap‘𝐾)‘𝑊)‘𝑡) ≠ (0g‘((LCDual‘𝐾)‘𝑊)))
6221, 26, 12, 13, 50, 52, 54, 57, 25, 61lvecvscan2 19430 . . . . 5 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (((𝐺‘(𝑋 · 𝑌))( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)) = (((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌))( ·𝑠 ‘((LCDual‘𝐾)‘𝑊))(((HDMap‘𝐾)‘𝑊)‘𝑡)) ↔ (𝐺‘(𝑋 · 𝑌)) = ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌))))
6349, 62mpbid 224 . . . 4 ((𝜑𝑡 ∈ (Base‘𝑈) ∧ 𝑡 ≠ (0g𝑈)) → (𝐺‘(𝑋 · 𝑌)) = ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌)))
6463rexlimdv3a 3213 . . 3 (𝜑 → (∃𝑡 ∈ (Base‘𝑈)𝑡 ≠ (0g𝑈) → (𝐺‘(𝑋 · 𝑌)) = ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌))))
656, 64mpd 15 . 2 (𝜑 → (𝐺‘(𝑋 · 𝑌)) = ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌)))
661, 2, 10, 11, 14, 5, 15hgmapcl 37903 . . 3 (𝜑 → (𝐺𝑋) ∈ 𝐵)
671, 2, 10, 11, 14, 5, 18hgmapcl 37903 . . 3 (𝜑 → (𝐺𝑌) ∈ 𝐵)
681, 2, 10, 11, 35, 7, 12, 27, 5, 66, 67lcdsmul 37616 . 2 (𝜑 → ((𝐺𝑋)(.r‘(Scalar‘((LCDual‘𝐾)‘𝑊)))(𝐺𝑌)) = ((𝐺𝑌) · (𝐺𝑋)))
6965, 68eqtrd 2832 1 (𝜑 → (𝐺‘(𝑋 · 𝑌)) = ((𝐺𝑌) · (𝐺𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108   = wceq 1653  wcel 2157  wne 2970  wrex 3089  cfv 6100  (class class class)co 6877  Basecbs 16181  .rcmulr 16265  Scalarcsca 16267   ·𝑠 cvsca 16268  0gc0g 16412  LModclmod 19178  LVecclvec 19420  HLchlt 35364  LHypclh 35998  DVecHcdvh 37092  LCDualclcd 37600  HDMapchdma 37806  HGMapchg 37897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-rep 4963  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-cnex 10279  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300  ax-riotaBAD 34967
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-ot 4376  df-uni 4628  df-int 4667  df-iun 4711  df-iin 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-om 7299  df-1st 7400  df-2nd 7401  df-tpos 7589  df-undef 7636  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-1o 7798  df-oadd 7802  df-er 7981  df-map 8096  df-en 8195  df-dom 8196  df-sdom 8197  df-fin 8198  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558  df-nn 11312  df-2 11373  df-3 11374  df-4 11375  df-5 11376  df-6 11377  df-n0 11578  df-z 11664  df-uz 11928  df-fz 12578  df-struct 16183  df-ndx 16184  df-slot 16185  df-base 16187  df-sets 16188  df-ress 16189  df-plusg 16277  df-mulr 16278  df-sca 16280  df-vsca 16281  df-0g 16414  df-mre 16558  df-mrc 16559  df-acs 16561  df-proset 17240  df-poset 17258  df-plt 17270  df-lub 17286  df-glb 17287  df-join 17288  df-meet 17289  df-p0 17351  df-p1 17352  df-lat 17358  df-clat 17420  df-mgm 17554  df-sgrp 17596  df-mnd 17607  df-submnd 17648  df-grp 17738  df-minusg 17739  df-sbg 17740  df-subg 17901  df-cntz 18059  df-oppg 18085  df-lsm 18361  df-cmn 18507  df-abl 18508  df-mgp 18803  df-ur 18815  df-ring 18862  df-oppr 18936  df-dvdsr 18954  df-unit 18955  df-invr 18985  df-dvr 18996  df-drng 19064  df-lmod 19180  df-lss 19248  df-lsp 19290  df-lvec 19421  df-lsatoms 34990  df-lshyp 34991  df-lcv 35033  df-lfl 35072  df-lkr 35100  df-ldual 35138  df-oposet 35190  df-ol 35192  df-oml 35193  df-covers 35280  df-ats 35281  df-atl 35312  df-cvlat 35336  df-hlat 35365  df-llines 35512  df-lplanes 35513  df-lvols 35514  df-lines 35515  df-psubsp 35517  df-pmap 35518  df-padd 35810  df-lhyp 36002  df-laut 36003  df-ldil 36118  df-ltrn 36119  df-trl 36173  df-tgrp 36757  df-tendo 36769  df-edring 36771  df-dveca 37017  df-disoa 37043  df-dvech 37093  df-dib 37153  df-dic 37187  df-dih 37243  df-doch 37362  df-djh 37409  df-lcdual 37601  df-mapd 37639  df-hvmap 37771  df-hdmap1 37807  df-hdmap 37808  df-hgmap 37898
This theorem is referenced by:  hgmapvvlem1  37937  hdmapglem7  37943  hlhilsrnglem  37967
  Copyright terms: Public domain W3C validator