![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcd0v2 | Structured version Visualization version GIF version |
Description: The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015.) |
Ref | Expression |
---|---|
lcd0v2.h | ⊢ 𝐻 = (LHyp‘𝐾) |
lcd0v2.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
lcd0v2.d | ⊢ 𝐷 = (LDual‘𝑈) |
lcd0v2.z | ⊢ 0 = (0g‘𝐷) |
lcd0v2.c | ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
lcd0v2.o | ⊢ 𝑂 = (0g‘𝐶) |
lcd0v2.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
Ref | Expression |
---|---|
lcd0v2 | ⊢ (𝜑 → 𝑂 = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcd0v2.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | lcd0v2.u | . . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
3 | eqid 2740 | . . 3 ⊢ (Base‘𝑈) = (Base‘𝑈) | |
4 | eqid 2740 | . . 3 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈) | |
5 | eqid 2740 | . . 3 ⊢ (0g‘(Scalar‘𝑈)) = (0g‘(Scalar‘𝑈)) | |
6 | lcd0v2.c | . . 3 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) | |
7 | lcd0v2.o | . . 3 ⊢ 𝑂 = (0g‘𝐶) | |
8 | lcd0v2.k | . . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | lcd0v 41561 | . 2 ⊢ (𝜑 → 𝑂 = ((Base‘𝑈) × {(0g‘(Scalar‘𝑈))})) |
10 | lcd0v2.d | . . 3 ⊢ 𝐷 = (LDual‘𝑈) | |
11 | lcd0v2.z | . . 3 ⊢ 0 = (0g‘𝐷) | |
12 | 1, 2, 8 | dvhlmod 41060 | . . 3 ⊢ (𝜑 → 𝑈 ∈ LMod) |
13 | 3, 4, 5, 10, 11, 12 | ldual0v 39099 | . 2 ⊢ (𝜑 → 0 = ((Base‘𝑈) × {(0g‘(Scalar‘𝑈))})) |
14 | 9, 13 | eqtr4d 2783 | 1 ⊢ (𝜑 → 𝑂 = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2108 {csn 4648 × cxp 5693 ‘cfv 6568 Basecbs 17252 Scalarcsca 17308 0gc0g 17493 LDualcld 39072 HLchlt 39299 LHypclh 39934 DVecHcdvh 41028 LCDualclcd 41536 |
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-2o 8517 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-mre 17638 df-mrc 17639 df-acs 17641 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-oppg 19380 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-nzr 20533 df-rlreg 20710 df-domn 20711 df-drng 20747 df-lmod 20876 df-lss 20947 df-lsp 20987 df-lvec 21119 df-lsatoms 38925 df-lshyp 38926 df-lcv 38968 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-lcdual 41537 |
This theorem is referenced by: lcdlkreqN 41572 hvmap1o2 41715 |
Copyright terms: Public domain | W3C validator |