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

Theorem hdmapfval 32690
 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 32689 . . . . 5 HDMap HDMap1 LCDual HVMap
54fveq1d 5732 . . . 4 HDMap HDMap1 LCDual HVMap
62, 5syl5eq 2482 . . 3 HDMap1 LCDual HVMap
7 fveq2 5730 . . . . . . . . . 10
87reseq2d 5148 . . . . . . . . 9
98opeq2d 3993 . . . . . . . 8
10 dfsbcq 3165 . . . . . . . 8 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
119, 10syl 16 . . . . . . 7 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
12 fveq2 5730 . . . . . . . . . 10
13 dfsbcq 3165 . . . . . . . . . 10 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
1412, 13syl 16 . . . . . . . . 9 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
15 fveq2 5730 . . . . . . . . . . . . 13 HDMap1 HDMap1
16 dfsbcq 3165 . . . . . . . . . . . . 13 HDMap1 HDMap1 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
1715, 16syl 16 . . . . . . . . . . . 12 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
18 fveq2 5730 . . . . . . . . . . . . . . . . 17 LCDual LCDual
1918fveq2d 5734 . . . . . . . . . . . . . . . 16 LCDual LCDual
20 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . 24 HVMap HVMap
2120fveq1d 5732 . . . . . . . . . . . . . . . . . . . . . . 23 HVMap HVMap
2221oteq2d 3999 . . . . . . . . . . . . . . . . . . . . . 22 HVMap HVMap
2322fveq2d 5734 . . . . . . . . . . . . . . . . . . . . 21 HVMap HVMap
2423oteq2d 3999 . . . . . . . . . . . . . . . . . . . 20 HVMap HVMap
2524fveq2d 5734 . . . . . . . . . . . . . . . . . . 19 HVMap HVMap
2625eqeq2d 2449 . . . . . . . . . . . . . . . . . 18 HVMap HVMap
2726imbi2d 309 . . . . . . . . . . . . . . . . 17 HVMap HVMap
2827ralbidv 2727 . . . . . . . . . . . . . . . 16 HVMap HVMap
2919, 28riotaeqbidv 6554 . . . . . . . . . . . . . . 15 LCDual HVMap LCDual HVMap
3029mpteq2dv 4298 . . . . . . . . . . . . . 14 LCDual HVMap LCDual HVMap
3130eleq2d 2505 . . . . . . . . . . . . 13 LCDual HVMap LCDual HVMap
3231sbcbidv 3217 . . . . . . . . . . . 12 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
3317, 32bitrd 246 . . . . . . . . . . 11 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
3433sbcbidv 3217 . . . . . . . . . 10 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
3534sbcbidv 3217 . . . . . . . . 9 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
3614, 35bitrd 246 . . . . . . . 8 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
3736sbcbidv 3217 . . . . . . 7 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
3811, 37bitrd 246 . . . . . 6 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
39 opex 4429 . . . . . . 7
40 fvex 5744 . . . . . . 7
41 fvex 5744 . . . . . . 7
42 simp1 958 . . . . . . . . 9
43 hdmapfval.e . . . . . . . . 9
4442, 43syl6eqr 2488 . . . . . . . 8
45 simp2 959 . . . . . . . . 9
46 hdmapfval.u . . . . . . . . 9
4745, 46syl6eqr 2488 . . . . . . . 8
48 simp3 960 . . . . . . . . . 10
4947fveq2d 5734 . . . . . . . . . 10
5048, 49eqtrd 2470 . . . . . . . . 9
51 hdmapfval.v . . . . . . . . 9
5250, 51syl6eqr 2488 . . . . . . . 8
53 fvex 5744 . . . . . . . . . 10 HDMap1
54 id 21 . . . . . . . . . . . 12 HDMap1 HDMap1
55 hdmapfval.i . . . . . . . . . . . 12 HDMap1
5654, 55syl6eqr 2488 . . . . . . . . . . 11 HDMap1
57 fveq1 5729 . . . . . . . . . . . . . . . . . 18 HVMap HVMap
58 fveq1 5729 . . . . . . . . . . . . . . . . . . . 20 HVMap HVMap
5958oteq2d 3999 . . . . . . . . . . . . . . . . . . 19 HVMap HVMap
6059fveq2d 5734 . . . . . . . . . . . . . . . . . 18 HVMap HVMap
6157, 60eqtrd 2470 . . . . . . . . . . . . . . . . 17 HVMap HVMap
6261eqeq2d 2449 . . . . . . . . . . . . . . . 16 HVMap HVMap
6362imbi2d 309 . . . . . . . . . . . . . . 15 HVMap HVMap
6463ralbidv 2727 . . . . . . . . . . . . . 14 HVMap HVMap
6564riotabidv 6553 . . . . . . . . . . . . 13 LCDual HVMap LCDual HVMap
6665mpteq2dv 4298 . . . . . . . . . . . 12 LCDual HVMap LCDual HVMap
6766eleq2d 2505 . . . . . . . . . . 11 LCDual HVMap LCDual HVMap
6856, 67syl 16 . . . . . . . . . 10 HDMap1 LCDual HVMap LCDual HVMap
6953, 68sbcie 3197 . . . . . . . . 9 HDMap1 LCDual HVMap LCDual HVMap
70 simp3 960 . . . . . . . . . . 11
71 hdmapfval.d . . . . . . . . . . . . . 14
72 hdmapfval.c . . . . . . . . . . . . . . 15 LCDual
7372fveq2i 5733 . . . . . . . . . . . . . 14 LCDual
7471, 73eqtr2i 2459 . . . . . . . . . . . . 13 LCDual
7574a1i 11 . . . . . . . . . . . 12 LCDual
76 simp2 959 . . . . . . . . . . . . . . . . . . . 20
7776fveq2d 5734 . . . . . . . . . . . . . . . . . . 19
78 hdmapfval.n . . . . . . . . . . . . . . . . . . 19
7977, 78syl6eqr 2488 . . . . . . . . . . . . . . . . . 18
80 simp1 958 . . . . . . . . . . . . . . . . . . 19
8180sneqd 3829 . . . . . . . . . . . . . . . . . 18
8279, 81fveq12d 5736 . . . . . . . . . . . . . . . . 17
8379fveq1d 5732 . . . . . . . . . . . . . . . . 17
8482, 83uneq12d 3504 . . . . . . . . . . . . . . . 16
8584eleq2d 2505 . . . . . . . . . . . . . . 15
8685notbid 287 . . . . . . . . . . . . . 14
8780oteq1d 3998 . . . . . . . . . . . . . . . . . . 19 HVMap HVMap
8880fveq2d 5734 . . . . . . . . . . . . . . . . . . . . 21 HVMap HVMap
89 hdmapfval.j . . . . . . . . . . . . . . . . . . . . . 22 HVMap
9089fveq1i 5731 . . . . . . . . . . . . . . . . . . . . 21 HVMap
9188, 90syl6eqr 2488 . . . . . . . . . . . . . . . . . . . 20 HVMap
9291oteq2d 3999 . . . . . . . . . . . . . . . . . . 19 HVMap
9387, 92eqtrd 2470 . . . . . . . . . . . . . . . . . 18 HVMap
9493fveq2d 5734 . . . . . . . . . . . . . . . . 17 HVMap
9594oteq2d 3999 . . . . . . . . . . . . . . . 16 HVMap
9695fveq2d 5734 . . . . . . . . . . . . . . 15 HVMap
9796eqeq2d 2449 . . . . . . . . . . . . . 14 HVMap
9886, 97imbi12d 313 . . . . . . . . . . . . 13 HVMap
9970, 98raleqbidv 2918 . . . . . . . . . . . 12 HVMap
10075, 99riotaeqbidv 6554 . . . . . . . . . . 11 LCDual HVMap
10170, 100mpteq12dv 4289 . . . . . . . . . 10 LCDual HVMap
102101eleq2d 2505 . . . . . . . . 9 LCDual HVMap
10369, 102syl5bb 250 . . . . . . . 8 HDMap1 LCDual HVMap
10444, 47, 52, 103syl3anc 1185 . . . . . . 7 HDMap1 LCDual HVMap
10539, 40, 41, 104sbc3ie 3232 . . . . . 6 HDMap1 LCDual HVMap
10638, 105syl6bb 254 . . . . 5 HDMap1 LCDual HVMap
107106abbi1dv 2554 . . . 4 HDMap1 LCDual HVMap
108 eqid 2438 . . . 4 HDMap1 LCDual HVMap HDMap1 LCDual HVMap
109 fvex 5744 . . . . . 6
11051, 109eqeltri 2508 . . . . 5
111110mptex 5968 . . . 4
112107, 108, 111fvmpt 5808 . . 3 HDMap1 LCDual HVMap
1136, 112sylan9eq 2490 . 2
1141, 113syl 16 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726  cab 2424  wral 2707  cvv 2958  wsbc 3163   cun 3320  csn 3816  cop 3819  cotp 3820   cmpt 4268   cid 4495   cres 4882  cfv 5456  crio 6544  cbs 13471  clspn 16049  clh 30843  cltrn 30960  cdvh 31938  LCDualclcd 32446  HVMapchvm 32616  HDMap1chdma1 32652  HDMapchdma 32653 This theorem is referenced by:  hdmapval  32691  hdmapfnN  32692 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pr 4405 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-ot 3826  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-riota 6551  df-hdmap 32655
 Copyright terms: Public domain W3C validator