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

Theorem hgmapfval 36686
 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 36685 . . . . 5 HGMap Scalar HDMap LCDual
54fveq1d 5866 . . . 4 HGMap Scalar HDMap LCDual
62, 5syl5eq 2520 . . 3 Scalar HDMap LCDual
7 fveq2 5864 . . . . . . . . 9
8 hgmapfval.u . . . . . . . . 9
97, 8syl6eqr 2526 . . . . . . . 8
10 dfsbcq 3333 . . . . . . . 8 Scalar HDMap LCDual Scalar HDMap LCDual
119, 10syl 16 . . . . . . 7 Scalar HDMap LCDual Scalar HDMap LCDual
12 fveq2 5864 . . . . . . . . . . . 12 HDMap HDMap
13 hgmapfval.m . . . . . . . . . . . 12 HDMap
1412, 13syl6eqr 2526 . . . . . . . . . . 11 HDMap
15 dfsbcq 3333 . . . . . . . . . . 11 HDMap HDMap LCDual LCDual
1614, 15syl 16 . . . . . . . . . 10 HDMap LCDual LCDual
17 fveq2 5864 . . . . . . . . . . . . . . . . . 18 LCDual LCDual
1817fveq2d 5868 . . . . . . . . . . . . . . . . 17 LCDual LCDual
1918oveqd 6299 . . . . . . . . . . . . . . . 16 LCDual LCDual
2019eqeq2d 2481 . . . . . . . . . . . . . . 15 LCDual LCDual
2120ralbidv 2903 . . . . . . . . . . . . . 14 LCDual LCDual
2221riotabidv 6245 . . . . . . . . . . . . 13 LCDual LCDual
2322mpteq2dv 4534 . . . . . . . . . . . 12 LCDual LCDual
2423eleq2d 2537 . . . . . . . . . . 11 LCDual LCDual
2524sbcbidv 3390 . . . . . . . . . 10 LCDual LCDual
2616, 25bitrd 253 . . . . . . . . 9 HDMap LCDual LCDual
2726sbcbidv 3390 . . . . . . . 8 Scalar HDMap LCDual Scalar LCDual
2827sbcbidv 3390 . . . . . . 7 Scalar HDMap LCDual Scalar LCDual
2911, 28bitrd 253 . . . . . 6 Scalar HDMap LCDual Scalar LCDual
30 fvex 5874 . . . . . . . 8
318, 30eqeltri 2551 . . . . . . 7
32 fvex 5874 . . . . . . 7 Scalar
33 fvex 5874 . . . . . . . 8 HDMap
3413, 33eqeltri 2551 . . . . . . 7
35 simp2 997 . . . . . . . . . 10 Scalar Scalar
36 simp1 996 . . . . . . . . . . . . 13 Scalar
3736fveq2d 5868 . . . . . . . . . . . 12 Scalar Scalar Scalar
38 hgmapfval.r . . . . . . . . . . . 12 Scalar
3937, 38syl6eqr 2526 . . . . . . . . . . 11 Scalar Scalar
4039fveq2d 5868 . . . . . . . . . 10 Scalar Scalar
4135, 40eqtrd 2508 . . . . . . . . 9 Scalar
42 hgmapfval.b . . . . . . . . 9
4341, 42syl6eqr 2526 . . . . . . . 8 Scalar
44 simp2 997 . . . . . . . . . 10
45 simp1 996 . . . . . . . . . . . . . 14
4645fveq2d 5868 . . . . . . . . . . . . 13
47 hgmapfval.v . . . . . . . . . . . . 13
4846, 47syl6eqr 2526 . . . . . . . . . . . 12
49 simp3 998 . . . . . . . . . . . . . 14
5045fveq2d 5868 . . . . . . . . . . . . . . . 16
51 hgmapfval.t . . . . . . . . . . . . . . . 16
5250, 51syl6eqr 2526 . . . . . . . . . . . . . . 15
5352oveqd 6299 . . . . . . . . . . . . . 14
5449, 53fveq12d 5870 . . . . . . . . . . . . 13
55 eqidd 2468 . . . . . . . . . . . . . . . . 17 LCDual LCDual
56 hgmapfval.c . . . . . . . . . . . . . . . . 17 LCDual
5755, 56syl6eqr 2526 . . . . . . . . . . . . . . . 16 LCDual
5857fveq2d 5868 . . . . . . . . . . . . . . 15 LCDual
59 hgmapfval.s . . . . . . . . . . . . . . 15
6058, 59syl6eqr 2526 . . . . . . . . . . . . . 14 LCDual
61 eqidd 2468 . . . . . . . . . . . . . 14
6249fveq1d 5866 . . . . . . . . . . . . . 14
6360, 61, 62oveq123d 6303 . . . . . . . . . . . . 13 LCDual
6454, 63eqeq12d 2489 . . . . . . . . . . . 12 LCDual
6548, 64raleqbidv 3072 . . . . . . . . . . 11 LCDual
6644, 65riotaeqbidv 6246 . . . . . . . . . 10 LCDual
6744, 66mpteq12dv 4525 . . . . . . . . 9 LCDual
6867eleq2d 2537 . . . . . . . 8 LCDual
6943, 68syld3an2 1275 . . . . . . 7 Scalar LCDual
7031, 32, 34, 69sbc3ie 3409 . . . . . 6 Scalar LCDual
7129, 70syl6bb 261 . . . . 5 Scalar HDMap LCDual
7271abbi1dv 2605 . . . 4 Scalar HDMap LCDual
73 eqid 2467 . . . 4 Scalar HDMap LCDual Scalar HDMap LCDual
74 fvex 5874 . . . . . 6
7542, 74eqeltri 2551 . . . . 5
7675mptex 6129 . . . 4
7772, 73, 76fvmpt 5948 . . 3 Scalar HDMap LCDual
786, 77sylan9eq 2528 . 2
791, 78syl 16 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 973   wceq 1379   wcel 1767  cab 2452  wral 2814  cvv 3113  wsbc 3331   cmpt 4505  cfv 5586  crio 6242  (class class class)co 6282  cbs 14486  Scalarcsca 14554  cvsca 14555  clh 34780  cdvh 35875  LCDualclcd 36383  HDMapchdma 36590  HGMapchg 36683 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pr 4686 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-hgmap 36684 This theorem is referenced by:  hgmapval  36687  hgmapfnN  36688
 Copyright terms: Public domain W3C validator