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 18690 | . 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
5 | 1, 4 | syl3an1 1163 | 1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ‘cfv 6491 (class class class)co 7349 Basecbs 17017 +gcplusg 17067 Grpcgrp 18682 LModclmod 20245 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 ax-nul 5261 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-iota 6443 df-fv 6499 df-ov 7352 df-mgm 18431 df-sgrp 18480 df-mnd 18491 df-grp 18685 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 37366 lfl0f 37426 lfladdcl 37428 lflnegcl 37432 lflvscl 37434 lkrlss 37452 lshpkrlem5 37471 lshpkrlem6 37472 dvh3dim2 39806 dvh3dim3N 39807 lcfrlem17 39917 lcfrlem19 39919 lcfrlem20 39920 lcfrlem23 39923 baerlem3lem1 40065 baerlem5alem1 40066 baerlem5blem1 40067 baerlem5alem2 40069 baerlem5blem2 40070 mapdindp0 40077 mapdindp2 40079 mapdindp4 40081 mapdh6lem2N 40092 mapdh6aN 40093 mapdh6dN 40097 mapdh6eN 40098 mapdh6hN 40101 hdmap1l6lem2 40166 hdmap1l6a 40167 hdmap1l6d 40171 hdmap1l6e 40172 hdmap1l6h 40175 hdmap11lem1 40199 hdmap11lem2 40200 hdmapneg 40204 hdmaprnlem3N 40208 hdmaprnlem3uN 40209 hdmaprnlem6N 40212 hdmaprnlem7N 40213 hdmaprnlem9N 40215 hdmaprnlem3eN 40216 hdmap14lem10 40235 hdmapinvlem3 40278 hdmapinvlem4 40279 hdmapglem7b 40286 hlhilphllem 40321 frlmsnic 40619 lincsumcl 46261 |
Copyright terms: Public domain | W3C validator |