Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmodvacl | Structured version Visualization version GIF version |
Description: Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
lmodvacl.v | ⊢ 𝑉 = (Base‘𝑊) |
lmodvacl.a | ⊢ + = (+g‘𝑊) |
Ref | Expression |
---|---|
lmodvacl | ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmodgrp 20252 | . 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | |
2 | lmodvacl.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
3 | lmodvacl.a | . . 3 ⊢ + = (+g‘𝑊) | |
4 | 2, 3 | grpcl 18691 | . 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
5 | 1, 4 | syl3an1 1164 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ‘cfv 6492 (class class class)co 7350 Basecbs 17018 +gcplusg 17068 Grpcgrp 18683 LModclmod 20245 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2709 ax-nul 5262 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-sbc 3739 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-iota 6444 df-fv 6500 df-ov 7353 df-mgm 18432 df-sgrp 18481 df-mnd 18492 df-grp 18686 df-lmod 20247 |
This theorem is referenced by: lmodcom 20291 lmodvsghm 20306 lss1 20322 lspprabs 20479 lspabs2 20504 lspabs3 20505 lspfixed 20512 lspexch 20513 lspsolvlem 20526 ipdir 20966 ipdi 20967 ip2di 20968 ocvlss 20999 frlmphl 21110 frlmup1 21127 nmparlem 24525 minveclem2 24712 lsatfixedN 37357 lfl0f 37417 lfladdcl 37419 lflnegcl 37423 lflvscl 37425 lkrlss 37443 lshpkrlem5 37462 lshpkrlem6 37463 dvh3dim2 39797 dvh3dim3N 39798 lcfrlem17 39908 lcfrlem19 39910 lcfrlem20 39911 lcfrlem23 39914 baerlem3lem1 40056 baerlem5alem1 40057 baerlem5blem1 40058 baerlem5alem2 40060 baerlem5blem2 40061 mapdindp0 40068 mapdindp2 40070 mapdindp4 40072 mapdh6lem2N 40083 mapdh6aN 40084 mapdh6dN 40088 mapdh6eN 40089 mapdh6hN 40092 hdmap1l6lem2 40157 hdmap1l6a 40158 hdmap1l6d 40162 hdmap1l6e 40163 hdmap1l6h 40166 hdmap11lem1 40190 hdmap11lem2 40191 hdmapneg 40195 hdmaprnlem3N 40199 hdmaprnlem3uN 40200 hdmaprnlem6N 40203 hdmaprnlem7N 40204 hdmaprnlem9N 40206 hdmaprnlem3eN 40207 hdmap14lem10 40226 hdmapinvlem3 40269 hdmapinvlem4 40270 hdmapglem7b 40277 hlhilphllem 40312 frlmsnic 40598 lincsumcl 46230 |
Copyright terms: Public domain | W3C validator |