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

Theorem hdmap1fval 35334
 Description: Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span to the convention for this section. (Contributed by NM, 15-May-2015.)
Hypotheses
Ref Expression
hdmap1val.h
hdmap1fval.u
hdmap1fval.v
hdmap1fval.s
hdmap1fval.o
hdmap1fval.n
hdmap1fval.c LCDual
hdmap1fval.d
hdmap1fval.r
hdmap1fval.q
hdmap1fval.j
hdmap1fval.m mapd
hdmap1fval.i HDMap1
hdmap1fval.k
Assertion
Ref Expression
hdmap1fval
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)   (,)   (,)   (,)   (,)   (,)

Proof of Theorem hdmap1fval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hdmap1fval.k . 2
2 hdmap1fval.i . . . 4 HDMap1
3 hdmap1val.h . . . . . 6
43hdmap1ffval 35333 . . . . 5 HDMap1 LCDual mapd
54fveq1d 5883 . . . 4 HDMap1 LCDual mapd
62, 5syl5eq 2475 . . 3 LCDual mapd
7 fveq2 5881 . . . . . . 7
8 fveq2 5881 . . . . . . . . . 10 LCDual LCDual
9 fveq2 5881 . . . . . . . . . . . . 13 mapd mapd
109sbceq1d 3304 . . . . . . . . . . . 12 mapd mapd
1110sbcbidv 3354 . . . . . . . . . . 11 mapd mapd
1211sbcbidv 3354 . . . . . . . . . 10 mapd mapd
138, 12sbceqbid 3306 . . . . . . . . 9 LCDual mapd LCDual mapd
1413sbcbidv 3354 . . . . . . . 8 LCDual mapd LCDual mapd
1514sbcbidv 3354 . . . . . . 7 LCDual mapd LCDual mapd
167, 15sbceqbid 3306 . . . . . 6 LCDual mapd LCDual mapd
17 fvex 5891 . . . . . . 7
18 fvex 5891 . . . . . . 7
19 fvex 5891 . . . . . . 7
20 hdmap1fval.u . . . . . . . . . . 11
2120eqeq2i 2440 . . . . . . . . . 10
2221biimpri 209 . . . . . . . . 9
23223ad2ant1 1026 . . . . . . . 8
24 simp2 1006 . . . . . . . . . 10
2522fveq2d 5885 . . . . . . . . . . 11
26253ad2ant1 1026 . . . . . . . . . 10
2724, 26eqtrd 2463 . . . . . . . . 9
28 hdmap1fval.v . . . . . . . . 9
2927, 28syl6eqr 2481 . . . . . . . 8
30 simp3 1007 . . . . . . . . . 10
3123fveq2d 5885 . . . . . . . . . 10
3230, 31eqtrd 2463 . . . . . . . . 9
33 hdmap1fval.n . . . . . . . . 9
3432, 33syl6eqr 2481 . . . . . . . 8
35 fvex 5891 . . . . . . . . . 10 LCDual
36 fvex 5891 . . . . . . . . . 10
37 fvex 5891 . . . . . . . . . 10
38 id 22 . . . . . . . . . . . . 13 LCDual LCDual
39 hdmap1fval.c . . . . . . . . . . . . 13 LCDual
4038, 39syl6eqr 2481 . . . . . . . . . . . 12 LCDual
41403ad2ant1 1026 . . . . . . . . . . 11 LCDual
42 simp2 1006 . . . . . . . . . . . 12 LCDual
4341fveq2d 5885 . . . . . . . . . . . . 13 LCDual
44 hdmap1fval.d . . . . . . . . . . . . 13
4543, 44syl6eqr 2481 . . . . . . . . . . . 12 LCDual
4642, 45eqtrd 2463 . . . . . . . . . . 11 LCDual
47 simp3 1007 . . . . . . . . . . . 12 LCDual
4841fveq2d 5885 . . . . . . . . . . . . 13 LCDual
49 hdmap1fval.j . . . . . . . . . . . . 13
5048, 49syl6eqr 2481 . . . . . . . . . . . 12 LCDual
5147, 50eqtrd 2463 . . . . . . . . . . 11 LCDual
52 fvex 5891 . . . . . . . . . . . . 13 mapd
53 id 22 . . . . . . . . . . . . . . 15 mapd mapd
54 hdmap1fval.m . . . . . . . . . . . . . . 15 mapd
5553, 54syl6eqr 2481 . . . . . . . . . . . . . 14 mapd
56 fveq1 5880 . . . . . . . . . . . . . . . . . . . 20
5756eqeq1d 2424 . . . . . . . . . . . . . . . . . . 19
58 fveq1 5880 . . . . . . . . . . . . . . . . . . . 20
5958eqeq1d 2424 . . . . . . . . . . . . . . . . . . 19
6057, 59anbi12d 715 . . . . . . . . . . . . . . . . . 18
6160riotabidv 6269 . . . . . . . . . . . . . . . . 17
6261ifeq2d 3930 . . . . . . . . . . . . . . . 16
6362mpteq2dv 4511 . . . . . . . . . . . . . . 15
6463eleq2d 2492 . . . . . . . . . . . . . 14
6555, 64syl 17 . . . . . . . . . . . . 13 mapd
6652, 65sbcie 3334 . . . . . . . . . . . 12 mapd
67 simp2 1006 . . . . . . . . . . . . . . 15
68 xpeq2 4868 . . . . . . . . . . . . . . . 16
6968xpeq1d 4876 . . . . . . . . . . . . . . 15
7067, 69syl 17 . . . . . . . . . . . . . 14
71 simp1 1005 . . . . . . . . . . . . . . . . 17
7271fveq2d 5885 . . . . . . . . . . . . . . . 16
73 hdmap1fval.q . . . . . . . . . . . . . . . 16
7472, 73syl6eqr 2481 . . . . . . . . . . . . . . 15
75 simp3 1007 . . . . . . . . . . . . . . . . . . 19
7675fveq1d 5883 . . . . . . . . . . . . . . . . . 18
7776eqeq2d 2436 . . . . . . . . . . . . . . . . 17
7871fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . 22
79 hdmap1fval.r . . . . . . . . . . . . . . . . . . . . . 22
8078, 79syl6eqr 2481 . . . . . . . . . . . . . . . . . . . . 21
8180oveqd 6322 . . . . . . . . . . . . . . . . . . . 20
8281sneqd 4010 . . . . . . . . . . . . . . . . . . 19
8375, 82fveq12d 5887 . . . . . . . . . . . . . . . . . 18
8483eqeq2d 2436 . . . . . . . . . . . . . . . . 17
8577, 84anbi12d 715 . . . . . . . . . . . . . . . 16
8667, 85riotaeqbidv 6270 . . . . . . . . . . . . . . 15
8774, 86ifeq12d 3931 . . . . . . . . . . . . . 14
8870, 87mpteq12dv 4502 . . . . . . . . . . . . 13
8988eleq2d 2492 . . . . . . . . . . . 12
9066, 89syl5bb 260 . . . . . . . . . . 11 mapd
9141, 46, 51, 90syl3anc 1264 . . . . . . . . . 10 LCDual mapd
9235, 36, 37, 91sbc3ie 3369 . . . . . . . . 9 LCDual mapd
93 simp2 1006 . . . . . . . . . . . . 13
9493xpeq1d 4876 . . . . . . . . . . . 12
9594, 93xpeq12d 4878 . . . . . . . . . . 11
96 simp1 1005 . . . . . . . . . . . . . . 15
9796fveq2d 5885 . . . . . . . . . . . . . 14
98 hdmap1fval.o . . . . . . . . . . . . . 14
9997, 98syl6eqr 2481 . . . . . . . . . . . . 13
10099eqeq2d 2436 . . . . . . . . . . . 12
101 simp3 1007 . . . . . . . . . . . . . . . . 17
102101fveq1d 5883 . . . . . . . . . . . . . . . 16
103102fveq2d 5885 . . . . . . . . . . . . . . 15
104103eqeq1d 2424 . . . . . . . . . . . . . 14
10596fveq2d 5885 . . . . . . . . . . . . . . . . . . . 20
106 hdmap1fval.s . . . . . . . . . . . . . . . . . . . 20
107105, 106syl6eqr 2481 . . . . . . . . . . . . . . . . . . 19
108107oveqd 6322 . . . . . . . . . . . . . . . . . 18
109108sneqd 4010 . . . . . . . . . . . . . . . . 17
110101, 109fveq12d 5887 . . . . . . . . . . . . . . . 16
111110fveq2d 5885 . . . . . . . . . . . . . . 15
112111eqeq1d 2424 . . . . . . . . . . . . . 14
113104, 112anbi12d 715 . . . . . . . . . . . . 13
114113riotabidv 6269 . . . . . . . . . . . 12
115100, 114ifbieq2d 3936 . . . . . . . . . . 11
11695, 115mpteq12dv 4502 . . . . . . . . . 10
117116eleq2d 2492 . . . . . . . . 9
11892, 117syl5bb 260 . . . . . . . 8 LCDual mapd
11923, 29, 34, 118syl3anc 1264 . . . . . . 7 LCDual mapd
12017, 18, 19, 119sbc3ie 3369 . . . . . 6 LCDual mapd
12116, 120syl6bb 264 . . . . 5 LCDual mapd
122121abbi1dv 2555 . . . 4 LCDual mapd
123 eqid 2422 . . . 4 LCDual mapd LCDual mapd
124 fvex 5891 . . . . . . . 8
12528, 124eqeltri 2503 . . . . . . 7
126 fvex 5891 . . . . . . . 8
12744, 126eqeltri 2503 . . . . . . 7
128125, 127xpex 6609 . . . . . 6
129128, 125xpex 6609 . . . . 5
130129mptex 6151 . . . 4
131122, 123, 130fvmpt 5964 . . 3 LCDual mapd
1326, 131sylan9eq 2483 . 2
1331, 132syl 17 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  cab 2407  cvv 3080  wsbc 3299  cif 3911  csn 3998   cmpt 4482   cxp 4851  cfv 5601  crio 6266  (class class class)co 6305  c1st 6805  c2nd 6806  cbs 15120  c0g 15337  csg 16670  clspn 18193  clh 33518  cdvh 34615  LCDualclcd 35123  mapdcmpd 35161  HDMap1chdma1 35329 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  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-ov 6308  df-hdmap1 35331 This theorem is referenced by:  hdmap1vallem  35335
 Copyright terms: Public domain W3C validator