Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nvgcl | Structured version Visualization version GIF version |
Description: Closure law for the vector addition (group) operation of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nvgcl.1 | β’ π = (BaseSetβπ) |
nvgcl.2 | β’ πΊ = ( +π£ βπ) |
Ref | Expression |
---|---|
nvgcl | β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvgcl.2 | . . 3 β’ πΊ = ( +π£ βπ) | |
2 | 1 | nvgrp 29024 | . 2 β’ (π β NrmCVec β πΊ β GrpOp) |
3 | nvgcl.1 | . . . 4 β’ π = (BaseSetβπ) | |
4 | 3, 1 | bafval 29011 | . . 3 β’ π = ran πΊ |
5 | 4 | grpocl 28907 | . 2 β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
6 | 2, 5 | syl3an1 1163 | 1 β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ w3a 1087 = wceq 1539 β wcel 2104 βcfv 6458 (class class class)co 7307 GrpOpcgr 28896 NrmCVeccnv 28991 +π£ cpv 28992 BaseSetcba 28993 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5218 ax-sep 5232 ax-nul 5239 ax-pr 5361 ax-un 7620 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-iun 4933 df-br 5082 df-opab 5144 df-mpt 5165 df-id 5500 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-ov 7310 df-oprab 7311 df-1st 7863 df-2nd 7864 df-grpo 28900 df-ablo 28952 df-vc 28966 df-nv 28999 df-va 29002 df-ba 29003 df-sm 29004 df-0v 29005 df-nmcv 29007 |
This theorem is referenced by: nvmf 29052 nvpncan2 29060 nvaddsub4 29064 nvdif 29073 nvpi 29074 nvabs 29079 imsmetlem 29097 vacn 29101 ipval2lem2 29111 4ipval2 29115 lnocoi 29164 0lno 29197 blocnilem 29211 ip0i 29232 ip1ilem 29233 ip2i 29235 ipdirilem 29236 ipasslem10 29246 dipdi 29250 ip2dii 29251 pythi 29257 ipblnfi 29262 ubthlem2 29278 minvecolem2 29282 hhshsslem2 29675 |
Copyright terms: Public domain | W3C validator |