Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nlmngp | Structured version Visualization version GIF version |
Description: A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
Ref | Expression |
---|---|
nlmngp | ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2738 | . . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊) | |
3 | eqid 2738 | . . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
4 | eqid 2738 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
5 | eqid 2738 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
6 | eqid 2738 | . . . 4 ⊢ (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊)) | |
7 | 1, 2, 3, 4, 5, 6 | isnlm 23597 | . . 3 ⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ (Base‘𝑊)((norm‘𝑊)‘(𝑥( ·𝑠 ‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦)))) |
8 | 7 | simplbi 501 | . 2 ⊢ (𝑊 ∈ NrmMod → (𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing)) |
9 | 8 | simp1d 1144 | 1 ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 = wceq 1543 ∈ wcel 2111 ∀wral 3062 ‘cfv 6398 (class class class)co 7232 · cmul 10759 Basecbs 16785 Scalarcsca 16830 ·𝑠 cvsca 16831 LModclmod 19924 normcnm 23498 NrmGrpcngp 23499 NrmRingcnrg 23501 NrmModcnlm 23502 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-nul 5214 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-rex 3068 df-rab 3071 df-v 3423 df-sbc 3710 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4253 df-if 4455 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4835 df-br 5069 df-iota 6356 df-fv 6406 df-ov 7235 df-nlm 23508 |
This theorem is referenced by: nlmdsdi 23603 nlmdsdir 23604 nlmmul0or 23605 nlmvscnlem2 23607 nlmvscnlem1 23608 nlmvscn 23609 nlmtlm 23616 lssnlm 23623 ngpocelbl 23626 isnmhm2 23674 idnmhm 23676 0nmhm 23677 nmoleub2lem 24035 nmoleub2lem3 24036 nmoleub2lem2 24037 nmoleub3 24040 nmhmcn 24041 ncvsm1 24075 ncvsdif 24076 ncvspi 24077 ncvs1 24078 ncvspds 24082 cphngp 24094 ipcnlem2 24165 ipcnlem1 24166 csscld 24170 bnngp 24263 cssbn 24296 |
Copyright terms: Public domain | W3C validator |