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

Theorem hgmapfval 34873
 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
hgmapfval.u
hgmapfval.v
hgmapfval.t
hgmapfval.r Scalar
hgmapfval.b
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
43hgmapffval 34872 . . . . 5 HGMap Scalar HDMap LCDual
54fveq1d 5805 . . . 4 HGMap Scalar HDMap LCDual
62, 5syl5eq 2453 . . 3 Scalar HDMap LCDual
7 fveq2 5803 . . . . . . . 8
8 hgmapfval.u . . . . . . . 8
97, 8syl6eqr 2459 . . . . . . 7
10 fveq2 5803 . . . . . . . . . 10 HDMap HDMap
11 hgmapfval.m . . . . . . . . . 10 HDMap
1210, 11syl6eqr 2459 . . . . . . . . 9 HDMap
13 fveq2 5803 . . . . . . . . . . . . . . . 16 LCDual LCDual
1413fveq2d 5807 . . . . . . . . . . . . . . 15 LCDual LCDual
1514oveqd 6249 . . . . . . . . . . . . . 14 LCDual LCDual
1615eqeq2d 2414 . . . . . . . . . . . . 13 LCDual LCDual
1716ralbidv 2840 . . . . . . . . . . . 12 LCDual LCDual
1817riotabidv 6196 . . . . . . . . . . 11 LCDual LCDual
1918mpteq2dv 4479 . . . . . . . . . 10 LCDual LCDual
2019eleq2d 2470 . . . . . . . . 9 LCDual LCDual
2112, 20sbceqbid 3281 . . . . . . . 8 HDMap LCDual LCDual
2221sbcbidv 3329 . . . . . . 7 Scalar HDMap LCDual Scalar LCDual
239, 22sbceqbid 3281 . . . . . 6 Scalar HDMap LCDual Scalar LCDual
24 fvex 5813 . . . . . . . 8
258, 24eqeltri 2484 . . . . . . 7
26 fvex 5813 . . . . . . 7 Scalar
27 fvex 5813 . . . . . . . 8 HDMap
2811, 27eqeltri 2484 . . . . . . 7
29 simp2 996 . . . . . . . . . 10 Scalar Scalar
30 simp1 995 . . . . . . . . . . . . 13 Scalar
3130fveq2d 5807 . . . . . . . . . . . 12 Scalar Scalar Scalar
32 hgmapfval.r . . . . . . . . . . . 12 Scalar
3331, 32syl6eqr 2459 . . . . . . . . . . 11 Scalar Scalar
3433fveq2d 5807 . . . . . . . . . 10 Scalar Scalar
3529, 34eqtrd 2441 . . . . . . . . 9 Scalar
36 hgmapfval.b . . . . . . . . 9
3735, 36syl6eqr 2459 . . . . . . . 8 Scalar
38 simp2 996 . . . . . . . . . 10
39 simp1 995 . . . . . . . . . . . . . 14
4039fveq2d 5807 . . . . . . . . . . . . 13
41 hgmapfval.v . . . . . . . . . . . . 13
4240, 41syl6eqr 2459 . . . . . . . . . . . 12
43 simp3 997 . . . . . . . . . . . . . 14
4439fveq2d 5807 . . . . . . . . . . . . . . . 16
45 hgmapfval.t . . . . . . . . . . . . . . . 16
4644, 45syl6eqr 2459 . . . . . . . . . . . . . . 15
4746oveqd 6249 . . . . . . . . . . . . . 14
4843, 47fveq12d 5809 . . . . . . . . . . . . 13
49 eqidd 2401 . . . . . . . . . . . . . . . . 17 LCDual LCDual
50 hgmapfval.c . . . . . . . . . . . . . . . . 17 LCDual
5149, 50syl6eqr 2459 . . . . . . . . . . . . . . . 16 LCDual
5251fveq2d 5807 . . . . . . . . . . . . . . 15 LCDual
53 hgmapfval.s . . . . . . . . . . . . . . 15
5452, 53syl6eqr 2459 . . . . . . . . . . . . . 14 LCDual
55 eqidd 2401 . . . . . . . . . . . . . 14
5643fveq1d 5805 . . . . . . . . . . . . . 14
5754, 55, 56oveq123d 6253 . . . . . . . . . . . . 13 LCDual
5848, 57eqeq12d 2422 . . . . . . . . . . . 12 LCDual
5942, 58raleqbidv 3015 . . . . . . . . . . 11 LCDual
6038, 59riotaeqbidv 6197 . . . . . . . . . 10 LCDual
6138, 60mpteq12dv 4470 . . . . . . . . 9 LCDual
6261eleq2d 2470 . . . . . . . 8 LCDual
6337, 62syld3an2 1275 . . . . . . 7 Scalar LCDual
6425, 26, 28, 63sbc3ie 3344 . . . . . 6 Scalar LCDual
6523, 64syl6bb 261 . . . . 5 Scalar HDMap LCDual
6665abbi1dv 2538 . . . 4 Scalar HDMap LCDual
67 eqid 2400 . . . 4 Scalar HDMap LCDual Scalar HDMap LCDual
68 fvex 5813 . . . . . 6
6936, 68eqeltri 2484 . . . . 5
7069mptex 6078 . . . 4
7166, 67, 70fvmpt 5886 . . 3 Scalar HDMap LCDual
726, 71sylan9eq 2461 . 2
731, 72syl 17 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   w3a 972   wceq 1403   wcel 1840  cab 2385  wral 2751  cvv 3056  wsbc 3274   cmpt 4450  cfv 5523  crio 6193  (class class class)co 6232  cbs 14731  Scalarcsca 14802  cvsca 14803  clh 32965  cdvh 34062  LCDualclcd 34570  HDMapchdma 34777  HGMapchg 34870 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pr 4627 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rex 2757  df-reu 2758  df-rab 2760  df-v 3058  df-sbc 3275  df-csb 3371  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-iun 4270  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4735  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5487  df-fun 5525  df-fn 5526  df-f 5527  df-f1 5528  df-fo 5529  df-f1o 5530  df-fv 5531  df-riota 6194  df-ov 6235  df-hgmap 34871 This theorem is referenced by:  hgmapval  34874  hgmapfnN  34875
 Copyright terms: Public domain W3C validator