![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > clmlmod | Structured version Visualization version GIF version |
Description: A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
Ref | Expression |
---|---|
clmlmod | ⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2724 | . . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
2 | eqid 2724 | . . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
3 | 1, 2 | isclm 24913 | . 2 ⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊))) ∧ (Base‘(Scalar‘𝑊)) ∈ (SubRing‘ℂfld))) |
4 | 3 | simp1bi 1142 | 1 ⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ‘cfv 6533 (class class class)co 7401 Basecbs 17143 ↾s cress 17172 Scalarcsca 17199 SubRingcsubrg 20459 LModclmod 20696 ℂfldccnfld 21228 ℂModcclm 24911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-nul 5296 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-ne 2933 df-rab 3425 df-v 3468 df-sbc 3770 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-iota 6485 df-fv 6541 df-ov 7404 df-clm 24912 |
This theorem is referenced by: clmgrp 24917 clmabl 24918 clmring 24919 clmfgrp 24920 clmvscl 24937 clmvsass 24938 clmvsdir 24940 clmvsdi 24941 clmvs1 24942 clmvs2 24943 clm0vs 24944 clmopfne 24945 clmvneg1 24948 clmvsneg 24949 clmsubdir 24951 clmvsubval 24958 zlmclm 24961 cmodscmulexp 24971 iscvs 24976 cvsi 24979 isncvsngp 24999 ttgbtwnid 28610 ttgcontlem1 28611 |
Copyright terms: Public domain | W3C validator |