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

Theorem hdmapfval 35107
 Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
Hypotheses
Ref Expression
hdmapval.h
hdmapfval.e
hdmapfval.u
hdmapfval.v
hdmapfval.n
hdmapfval.c LCDual
hdmapfval.d
hdmapfval.j HVMap
hdmapfval.i HDMap1
hdmapfval.s HDMap
hdmapfval.k
Assertion
Ref Expression
hdmapfval
Distinct variable groups:   ,,,   ,   ,,,   ,,,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)   (,,)   (,)   (,,)   (,,)   (,,)   (,,)

Proof of Theorem hdmapfval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hdmapfval.k . 2
2 hdmapfval.s . . . 4 HDMap
3 hdmapval.h . . . . . 6
43hdmapffval 35106 . . . . 5 HDMap HDMap1 LCDual HVMap
54fveq1d 5883 . . . 4 HDMap HDMap1 LCDual HVMap
62, 5syl5eq 2482 . . 3 HDMap1 LCDual HVMap
7 fveq2 5881 . . . . . . . . 9
87reseq2d 5125 . . . . . . . 8
98opeq2d 4197 . . . . . . 7
10 fveq2 5881 . . . . . . . 8
11 fveq2 5881 . . . . . . . . . 10 HDMap1 HDMap1
12 fveq2 5881 . . . . . . . . . . . . . 14 LCDual LCDual
1312fveq2d 5885 . . . . . . . . . . . . 13 LCDual LCDual
14 fveq2 5881 . . . . . . . . . . . . . . . . . . . . 21 HVMap HVMap
1514fveq1d 5883 . . . . . . . . . . . . . . . . . . . 20 HVMap HVMap
1615oteq2d 4203 . . . . . . . . . . . . . . . . . . 19 HVMap HVMap
1716fveq2d 5885 . . . . . . . . . . . . . . . . . 18 HVMap HVMap
1817oteq2d 4203 . . . . . . . . . . . . . . . . 17 HVMap HVMap
1918fveq2d 5885 . . . . . . . . . . . . . . . 16 HVMap HVMap
2019eqeq2d 2443 . . . . . . . . . . . . . . 15 HVMap HVMap
2120imbi2d 317 . . . . . . . . . . . . . 14 HVMap HVMap
2221ralbidv 2871 . . . . . . . . . . . . 13 HVMap HVMap
2313, 22riotaeqbidv 6270 . . . . . . . . . . . 12 LCDual HVMap LCDual HVMap
2423mpteq2dv 4513 . . . . . . . . . . 11 LCDual HVMap LCDual HVMap
2524eleq2d 2499 . . . . . . . . . 10 LCDual HVMap LCDual HVMap
2611, 25sbceqbid 3312 . . . . . . . . 9 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
2726sbcbidv 3360 . . . . . . . 8 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
2810, 27sbceqbid 3312 . . . . . . 7 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
299, 28sbceqbid 3312 . . . . . 6 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
30 opex 4686 . . . . . . 7
31 fvex 5891 . . . . . . 7
32 fvex 5891 . . . . . . 7
33 simp1 1005 . . . . . . . . 9
34 hdmapfval.e . . . . . . . . 9
3533, 34syl6eqr 2488 . . . . . . . 8
36 simp2 1006 . . . . . . . . 9
37 hdmapfval.u . . . . . . . . 9
3836, 37syl6eqr 2488 . . . . . . . 8
39 simp3 1007 . . . . . . . . . 10
4038fveq2d 5885 . . . . . . . . . 10
4139, 40eqtrd 2470 . . . . . . . . 9
42 hdmapfval.v . . . . . . . . 9
4341, 42syl6eqr 2488 . . . . . . . 8
44 fvex 5891 . . . . . . . . . 10 HDMap1
45 id 23 . . . . . . . . . . . 12 HDMap1 HDMap1
46 hdmapfval.i . . . . . . . . . . . 12 HDMap1
4745, 46syl6eqr 2488 . . . . . . . . . . 11 HDMap1
48 fveq1 5880 . . . . . . . . . . . . . . . . . 18 HVMap HVMap
49 fveq1 5880 . . . . . . . . . . . . . . . . . . . 20 HVMap HVMap
5049oteq2d 4203 . . . . . . . . . . . . . . . . . . 19 HVMap HVMap
5150fveq2d 5885 . . . . . . . . . . . . . . . . . 18 HVMap HVMap
5248, 51eqtrd 2470 . . . . . . . . . . . . . . . . 17 HVMap HVMap
5352eqeq2d 2443 . . . . . . . . . . . . . . . 16 HVMap HVMap
5453imbi2d 317 . . . . . . . . . . . . . . 15 HVMap HVMap
5554ralbidv 2871 . . . . . . . . . . . . . 14 HVMap HVMap
5655riotabidv 6269 . . . . . . . . . . . . 13 LCDual HVMap LCDual HVMap
5756mpteq2dv 4513 . . . . . . . . . . . 12 LCDual HVMap LCDual HVMap
5857eleq2d 2499 . . . . . . . . . . 11 LCDual HVMap LCDual HVMap
5947, 58syl 17 . . . . . . . . . 10 HDMap1 LCDual HVMap LCDual HVMap
6044, 59sbcie 3340 . . . . . . . . 9 HDMap1 LCDual HVMap LCDual HVMap
61 simp3 1007 . . . . . . . . . . 11
62 hdmapfval.d . . . . . . . . . . . . . 14
63 hdmapfval.c . . . . . . . . . . . . . . 15 LCDual
6463fveq2i 5884 . . . . . . . . . . . . . 14 LCDual
6562, 64eqtr2i 2459 . . . . . . . . . . . . 13 LCDual
6665a1i 11 . . . . . . . . . . . 12 LCDual
67 simp2 1006 . . . . . . . . . . . . . . . . . . . 20
6867fveq2d 5885 . . . . . . . . . . . . . . . . . . 19
69 hdmapfval.n . . . . . . . . . . . . . . . . . . 19
7068, 69syl6eqr 2488 . . . . . . . . . . . . . . . . . 18
71 simp1 1005 . . . . . . . . . . . . . . . . . . 19
7271sneqd 4014 . . . . . . . . . . . . . . . . . 18
7370, 72fveq12d 5887 . . . . . . . . . . . . . . . . 17
7470fveq1d 5883 . . . . . . . . . . . . . . . . 17
7573, 74uneq12d 3627 . . . . . . . . . . . . . . . 16
7675eleq2d 2499 . . . . . . . . . . . . . . 15
7776notbid 295 . . . . . . . . . . . . . 14
7871oteq1d 4202 . . . . . . . . . . . . . . . . . . 19 HVMap HVMap
7971fveq2d 5885 . . . . . . . . . . . . . . . . . . . . 21 HVMap HVMap
80 hdmapfval.j . . . . . . . . . . . . . . . . . . . . . 22 HVMap
8180fveq1i 5882 . . . . . . . . . . . . . . . . . . . . 21 HVMap
8279, 81syl6eqr 2488 . . . . . . . . . . . . . . . . . . . 20 HVMap
8382oteq2d 4203 . . . . . . . . . . . . . . . . . . 19 HVMap
8478, 83eqtrd 2470 . . . . . . . . . . . . . . . . . 18 HVMap
8584fveq2d 5885 . . . . . . . . . . . . . . . . 17 HVMap
8685oteq2d 4203 . . . . . . . . . . . . . . . 16 HVMap
8786fveq2d 5885 . . . . . . . . . . . . . . 15 HVMap
8887eqeq2d 2443 . . . . . . . . . . . . . 14 HVMap
8977, 88imbi12d 321 . . . . . . . . . . . . 13 HVMap
9061, 89raleqbidv 3046 . . . . . . . . . . . 12 HVMap
9166, 90riotaeqbidv 6270 . . . . . . . . . . 11 LCDual HVMap
9261, 91mpteq12dv 4504 . . . . . . . . . 10 LCDual HVMap
9392eleq2d 2499 . . . . . . . . 9 LCDual HVMap
9460, 93syl5bb 260 . . . . . . . 8 HDMap1 LCDual HVMap
9535, 38, 43, 94syl3anc 1264 . . . . . . 7 HDMap1 LCDual HVMap
9630, 31, 32, 95sbc3ie 3375 . . . . . 6 HDMap1 LCDual HVMap
9729, 96syl6bb 264 . . . . 5 HDMap1 LCDual HVMap
9897abbi1dv 2567 . . . 4 HDMap1 LCDual HVMap
99 eqid 2429 . . . 4 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
100 fvex 5891 . . . . . 6
10142, 100eqeltri 2513 . . . . 5
102101mptex 6151 . . . 4
10398, 99, 102fvmpt 5964 . . 3 HDMap1 LCDual HVMap
1046, 103sylan9eq 2490 . 2
1051, 104syl 17 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1870  cab 2414  wral 2782  cvv 3087  wsbc 3305   cun 3440  csn 4002  cop 4008  cotp 4010   cmpt 4484   cid 4764   cres 4856  cfv 5601  crio 6266  cbs 15084  clspn 18129  clh 33258  cltrn 33375  cdvh 34355  LCDualclcd 34863  HVMapchvm 35033  HDMap1chdma1 35069  HDMapchdma 35070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pr 4661 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-ot 4011  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-hdmap 35072 This theorem is referenced by:  hdmapval  35108  hdmapfnN  35109
 Copyright terms: Public domain W3C validator