![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hvmapclN | Structured version Visualization version GIF version |
Description: Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hvmap1o.h | ⊢ 𝐻 = (LHyp‘𝐾) |
hvmap1o.o | ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
hvmap1o.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
hvmap1o.v | ⊢ 𝑉 = (Base‘𝑈) |
hvmap1o.z | ⊢ 0 = (0g‘𝑈) |
hvmap1o.f | ⊢ 𝐹 = (LFnl‘𝑈) |
hvmap1o.l | ⊢ 𝐿 = (LKer‘𝑈) |
hvmap1o.d | ⊢ 𝐷 = (LDual‘𝑈) |
hvmap1o.q | ⊢ 𝑄 = (0g‘𝐷) |
hvmap1o.c | ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
hvmap1o.m | ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) |
hvmap1o.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
hvmapcl.x | ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
Ref | Expression |
---|---|
hvmapclN | ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐶 ∖ {𝑄})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hvmap1o.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | hvmap1o.o | . . . 4 ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) | |
3 | hvmap1o.u | . . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
4 | hvmap1o.v | . . . 4 ⊢ 𝑉 = (Base‘𝑈) | |
5 | hvmap1o.z | . . . 4 ⊢ 0 = (0g‘𝑈) | |
6 | hvmap1o.f | . . . 4 ⊢ 𝐹 = (LFnl‘𝑈) | |
7 | hvmap1o.l | . . . 4 ⊢ 𝐿 = (LKer‘𝑈) | |
8 | hvmap1o.d | . . . 4 ⊢ 𝐷 = (LDual‘𝑈) | |
9 | hvmap1o.q | . . . 4 ⊢ 𝑄 = (0g‘𝐷) | |
10 | hvmap1o.c | . . . 4 ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓)} | |
11 | hvmap1o.m | . . . 4 ⊢ 𝑀 = ((HVMap‘𝐾)‘𝑊) | |
12 | hvmap1o.k | . . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | hvmap1o 41713 | . . 3 ⊢ (𝜑 → 𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐶 ∖ {𝑄})) |
14 | f1of 6857 | . . 3 ⊢ (𝑀:(𝑉 ∖ { 0 })–1-1-onto→(𝐶 ∖ {𝑄}) → 𝑀:(𝑉 ∖ { 0 })⟶(𝐶 ∖ {𝑄})) | |
15 | 13, 14 | syl 17 | . 2 ⊢ (𝜑 → 𝑀:(𝑉 ∖ { 0 })⟶(𝐶 ∖ {𝑄})) |
16 | hvmapcl.x | . 2 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | |
17 | 15, 16 | ffvelcdmd 7114 | 1 ⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐶 ∖ {𝑄})) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2108 {crab 3443 ∖ cdif 3973 {csn 4648 ⟶wf 6564 –1-1-onto→wf1o 6567 ‘cfv 6568 Basecbs 17252 0gc0g 17493 LFnlclfn 39006 LKerclk 39034 LDualcld 39072 HLchlt 39299 LHypclh 39934 DVecHcdvh 41028 ocHcoch 41297 HVMapchvm 41706 |
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 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7764 ax-cnex 11234 ax-resscn 11235 ax-1cn 11236 ax-icn 11237 ax-addcl 11238 ax-addrcl 11239 ax-mulcl 11240 ax-mulrcl 11241 ax-mulcom 11242 ax-addass 11243 ax-mulass 11244 ax-distr 11245 ax-i2m1 11246 ax-1ne0 11247 ax-1rid 11248 ax-rnegex 11249 ax-rrecex 11250 ax-cnre 11251 ax-pre-lttri 11252 ax-pre-lttrn 11253 ax-pre-ltadd 11254 ax-pre-mulgt0 11255 ax-riotaBAD 38902 |
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 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5650 df-we 5652 df-xp 5701 df-rel 5702 df-cnv 5703 df-co 5704 df-dm 5705 df-rn 5706 df-res 5707 df-ima 5708 df-pred 6327 df-ord 6393 df-on 6394 df-lim 6395 df-suc 6396 df-iota 6520 df-fun 6570 df-fn 6571 df-f 6572 df-f1 6573 df-fo 6574 df-f1o 6575 df-fv 6576 df-riota 7399 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7708 df-om 7898 df-1st 8024 df-2nd 8025 df-tpos 8261 df-undef 8308 df-frecs 8316 df-wrecs 8347 df-recs 8421 df-rdg 8460 df-1o 8516 df-er 8757 df-map 8880 df-en 8998 df-dom 8999 df-sdom 9000 df-fin 9001 df-pnf 11320 df-mnf 11321 df-xr 11322 df-ltxr 11323 df-le 11324 df-sub 11516 df-neg 11517 df-nn 12288 df-2 12350 df-3 12351 df-4 12352 df-5 12353 df-6 12354 df-n0 12548 df-z 12634 df-uz 12898 df-fz 13562 df-struct 17188 df-sets 17205 df-slot 17223 df-ndx 17235 df-base 17253 df-ress 17282 df-plusg 17318 df-mulr 17319 df-sca 17321 df-vsca 17322 df-0g 17495 df-proset 18359 df-poset 18377 df-plt 18394 df-lub 18410 df-glb 18411 df-join 18412 df-meet 18413 df-p0 18489 df-p1 18490 df-lat 18496 df-clat 18563 df-mgm 18672 df-sgrp 18751 df-mnd 18767 df-submnd 18813 df-grp 18970 df-minusg 18971 df-sbg 18972 df-subg 19157 df-cntz 19351 df-lsm 19672 df-cmn 19818 df-abl 19819 df-mgp 20156 df-rng 20174 df-ur 20203 df-ring 20256 df-oppr 20354 df-dvdsr 20377 df-unit 20378 df-invr 20408 df-dvr 20421 df-drng 20747 df-lmod 20876 df-lss 20947 df-lsp 20987 df-lvec 21119 df-lsatoms 38925 df-lshyp 38926 df-lfl 39007 df-lkr 39035 df-ldual 39073 df-oposet 39125 df-ol 39127 df-oml 39128 df-covers 39215 df-ats 39216 df-atl 39247 df-cvlat 39271 df-hlat 39300 df-llines 39448 df-lplanes 39449 df-lvols 39450 df-lines 39451 df-psubsp 39453 df-pmap 39454 df-padd 39746 df-lhyp 39938 df-laut 39939 df-ldil 40054 df-ltrn 40055 df-trl 40109 df-tgrp 40693 df-tendo 40705 df-edring 40707 df-dveca 40953 df-disoa 40979 df-dvech 41029 df-dib 41089 df-dic 41123 df-dih 41179 df-doch 41298 df-djh 41345 df-hvmap 41707 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |