Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hvmap1o2 Structured version   Visualization version   GIF version

Theorem hvmap1o2 41742
Description: The vector to functional map provides a bijection from nonzero vectors 𝑉 to nonzero functionals with closed kernels 𝐶. (Contributed by NM, 27-Mar-2015.)
Hypotheses
Ref Expression
hvmap1o2.h 𝐻 = (LHyp‘𝐾)
hvmap1o2.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
hvmap1o2.v 𝑉 = (Base‘𝑈)
hvmap1o2.z 0 = (0g𝑈)
hvmap1o2.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
hvmap1o2.f 𝐹 = (Base‘𝐶)
hvmap1o2.o 𝑂 = (0g𝐶)
hvmap1o2.m 𝑀 = ((HVMap‘𝐾)‘𝑊)
hvmap1o2.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
Assertion
Ref Expression
hvmap1o2 (𝜑𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐹 ∖ {𝑂}))

Proof of Theorem hvmap1o2
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 hvmap1o2.h . . 3 𝐻 = (LHyp‘𝐾)
2 eqid 2740 . . 3 ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
3 hvmap1o2.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
4 hvmap1o2.v . . 3 𝑉 = (Base‘𝑈)
5 hvmap1o2.z . . 3 0 = (0g𝑈)
6 eqid 2740 . . 3 (LFnl‘𝑈) = (LFnl‘𝑈)
7 eqid 2740 . . 3 (LKer‘𝑈) = (LKer‘𝑈)
8 eqid 2740 . . 3 (LDual‘𝑈) = (LDual‘𝑈)
9 eqid 2740 . . 3 (0g‘(LDual‘𝑈)) = (0g‘(LDual‘𝑈))
10 eqid 2740 . . 3 {𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)}
11 hvmap1o2.m . . 3 𝑀 = ((HVMap‘𝐾)‘𝑊)
12 hvmap1o2.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12hvmap1o 41740 . 2 (𝜑𝑀:(𝑉 ∖ { 0 })–1-1-onto→({𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)} ∖ {(0g‘(LDual‘𝑈))}))
14 hvmap1o2.c . . . . 5 𝐶 = ((LCDual‘𝐾)‘𝑊)
15 hvmap1o2.f . . . . 5 𝐹 = (Base‘𝐶)
161, 2, 14, 15, 3, 6, 7, 10, 12lcdvbase 41570 . . . 4 (𝜑𝐹 = {𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)})
17 hvmap1o2.o . . . . . 6 𝑂 = (0g𝐶)
181, 3, 8, 9, 14, 17, 12lcd0v2 41589 . . . . 5 (𝜑𝑂 = (0g‘(LDual‘𝑈)))
1918sneqd 4660 . . . 4 (𝜑 → {𝑂} = {(0g‘(LDual‘𝑈))})
2016, 19difeq12d 4150 . . 3 (𝜑 → (𝐹 ∖ {𝑂}) = ({𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)} ∖ {(0g‘(LDual‘𝑈))}))
21 f1oeq3 6855 . . 3 ((𝐹 ∖ {𝑂}) = ({𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)} ∖ {(0g‘(LDual‘𝑈))}) → (𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐹 ∖ {𝑂}) ↔ 𝑀:(𝑉 ∖ { 0 })–1-1-onto→({𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)} ∖ {(0g‘(LDual‘𝑈))})))
2220, 21syl 17 . 2 (𝜑 → (𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐹 ∖ {𝑂}) ↔ 𝑀:(𝑉 ∖ { 0 })–1-1-onto→({𝑓 ∈ (LFnl‘𝑈) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘𝑈)‘𝑓))) = ((LKer‘𝑈)‘𝑓)} ∖ {(0g‘(LDual‘𝑈))})))
2313, 22mpbird 257 1 (𝜑𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐹 ∖ {𝑂}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2108  {crab 3443  cdif 3973  {csn 4648  1-1-ontowf1o 6575  cfv 6576  Basecbs 17278  0gc0g 17519  LFnlclfn 39033  LKerclk 39061  LDualcld 39099  HLchlt 39326  LHypclh 39961  DVecHcdvh 41055  ocHcoch 41324  LCDualclcd 41563  HVMapchvm 41733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5304  ax-sep 5318  ax-nul 5325  ax-pow 5384  ax-pr 5448  ax-un 7773  ax-cnex 11243  ax-resscn 11244  ax-1cn 11245  ax-icn 11246  ax-addcl 11247  ax-addrcl 11248  ax-mulcl 11249  ax-mulrcl 11250  ax-mulcom 11251  ax-addass 11252  ax-mulass 11253  ax-distr 11254  ax-i2m1 11255  ax-1ne0 11256  ax-1rid 11257  ax-rnegex 11258  ax-rrecex 11259  ax-cnre 11260  ax-pre-lttri 11261  ax-pre-lttrn 11262  ax-pre-ltadd 11263  ax-pre-mulgt0 11264  ax-riotaBAD 38929
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4933  df-int 4972  df-iun 5018  df-iin 5019  df-br 5168  df-opab 5230  df-mpt 5251  df-tr 5285  df-id 5594  df-eprel 5600  df-po 5608  df-so 5609  df-fr 5653  df-we 5655  df-xp 5707  df-rel 5708  df-cnv 5709  df-co 5710  df-dm 5711  df-rn 5712  df-res 5713  df-ima 5714  df-pred 6335  df-ord 6401  df-on 6402  df-lim 6403  df-suc 6404  df-iota 6528  df-fun 6578  df-fn 6579  df-f 6580  df-f1 6581  df-fo 6582  df-f1o 6583  df-fv 6584  df-riota 7407  df-ov 7454  df-oprab 7455  df-mpo 7456  df-of 7717  df-om 7907  df-1st 8033  df-2nd 8034  df-tpos 8270  df-undef 8317  df-frecs 8325  df-wrecs 8356  df-recs 8430  df-rdg 8469  df-1o 8525  df-2o 8526  df-er 8766  df-map 8889  df-en 9007  df-dom 9008  df-sdom 9009  df-fin 9010  df-pnf 11329  df-mnf 11330  df-xr 11331  df-ltxr 11332  df-le 11333  df-sub 11526  df-neg 11527  df-nn 12299  df-2 12361  df-3 12362  df-4 12363  df-5 12364  df-6 12365  df-n0 12559  df-z 12646  df-uz 12911  df-fz 13579  df-struct 17214  df-sets 17231  df-slot 17249  df-ndx 17261  df-base 17279  df-ress 17308  df-plusg 17344  df-mulr 17345  df-sca 17347  df-vsca 17348  df-0g 17521  df-mre 17664  df-mrc 17665  df-acs 17667  df-proset 18385  df-poset 18403  df-plt 18420  df-lub 18436  df-glb 18437  df-join 18438  df-meet 18439  df-p0 18515  df-p1 18516  df-lat 18522  df-clat 18589  df-mgm 18698  df-sgrp 18777  df-mnd 18793  df-submnd 18839  df-grp 18996  df-minusg 18997  df-sbg 18998  df-subg 19183  df-cntz 19377  df-oppg 19406  df-lsm 19698  df-cmn 19844  df-abl 19845  df-mgp 20182  df-rng 20200  df-ur 20229  df-ring 20282  df-oppr 20380  df-dvdsr 20403  df-unit 20404  df-invr 20434  df-dvr 20447  df-nzr 20559  df-rlreg 20736  df-domn 20737  df-drng 20773  df-lmod 20902  df-lss 20973  df-lsp 21013  df-lvec 21145  df-lsatoms 38952  df-lshyp 38953  df-lcv 38995  df-lfl 39034  df-lkr 39062  df-ldual 39100  df-oposet 39152  df-ol 39154  df-oml 39155  df-covers 39242  df-ats 39243  df-atl 39274  df-cvlat 39298  df-hlat 39327  df-llines 39475  df-lplanes 39476  df-lvols 39477  df-lines 39478  df-psubsp 39480  df-pmap 39481  df-padd 39773  df-lhyp 39965  df-laut 39966  df-ldil 40081  df-ltrn 40082  df-trl 40136  df-tgrp 40720  df-tendo 40732  df-edring 40734  df-dveca 40980  df-disoa 41006  df-dvech 41056  df-dib 41116  df-dic 41150  df-dih 41206  df-doch 41325  df-djh 41372  df-lcdual 41564  df-hvmap 41734
This theorem is referenced by:  hvmapcl2  41743
  Copyright terms: Public domain W3C validator