![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmodgrp | Structured version Visualization version GIF version |
Description: A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
Ref | Expression |
---|---|
lmodgrp | β’ (π β LMod β π β Grp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2733 | . . 3 β’ (Baseβπ) = (Baseβπ) | |
2 | eqid 2733 | . . 3 β’ (+gβπ) = (+gβπ) | |
3 | eqid 2733 | . . 3 β’ ( Β·π βπ) = ( Β·π βπ) | |
4 | eqid 2733 | . . 3 β’ (Scalarβπ) = (Scalarβπ) | |
5 | eqid 2733 | . . 3 β’ (Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) | |
6 | eqid 2733 | . . 3 β’ (+gβ(Scalarβπ)) = (+gβ(Scalarβπ)) | |
7 | eqid 2733 | . . 3 β’ (.rβ(Scalarβπ)) = (.rβ(Scalarβπ)) | |
8 | eqid 2733 | . . 3 β’ (1rβ(Scalarβπ)) = (1rβ(Scalarβπ)) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | islmod 20475 | . 2 β’ (π β LMod β (π β Grp β§ (Scalarβπ) β Ring β§ βπ β (Baseβ(Scalarβπ))βπ β (Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ€ β (Baseβπ)(((π( Β·π βπ)π€) β (Baseβπ) β§ (π( Β·π βπ)(π€(+gβπ)π₯)) = ((π( Β·π βπ)π€)(+gβπ)(π( Β·π βπ)π₯)) β§ ((π(+gβ(Scalarβπ))π)( Β·π βπ)π€) = ((π( Β·π βπ)π€)(+gβπ)(π( Β·π βπ)π€))) β§ (((π(.rβ(Scalarβπ))π)( Β·π βπ)π€) = (π( Β·π βπ)(π( Β·π βπ)π€)) β§ ((1rβ(Scalarβπ))( Β·π βπ)π€) = π€)))) |
10 | 9 | simp1bi 1146 | 1 β’ (π β LMod β π β Grp) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 397 β§ w3a 1088 = wceq 1542 β wcel 2107 βwral 3062 βcfv 6544 (class class class)co 7409 Basecbs 17144 +gcplusg 17197 .rcmulr 17198 Scalarcsca 17200 Β·π cvsca 17201 Grpcgrp 18819 1rcur 20004 Ringcrg 20056 LModclmod 20471 |
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 2704 ax-nul 5307 |
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 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rab 3434 df-v 3477 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-ov 7412 df-lmod 20473 |
This theorem is referenced by: lmodgrpd 20481 lmodbn0 20482 lmodvacl 20486 lmodass 20487 lmodlcan 20488 lmod0vcl 20501 lmod0vlid 20502 lmod0vrid 20503 lmod0vid 20504 lmodvsmmulgdi 20507 lmodfopne 20510 lmodvnegcl 20513 lmodvnegid 20514 lmodvsubcl 20517 lmodcom 20518 lmodabl 20519 lmodvpncan 20525 lmodvnpcan 20526 lmodsubeq0 20531 lmodsubid 20532 lmodvsghm 20533 lmodprop2d 20534 lsssubg 20568 islss3 20570 lssacs 20578 prdslmodd 20580 lspsnneg 20617 lspsnsub 20618 lmodindp1 20625 lmodvsinv2 20648 islmhm2 20649 0lmhm 20651 idlmhm 20652 pwsdiaglmhm 20668 pwssplit3 20672 lspexch 20742 lspsolvlem 20755 ip0l 21189 ipsubdir 21195 ipsubdi 21196 ip2eq 21206 lsmcss 21245 dsmmlss 21299 frlm0 21309 frlmsubgval 21320 frlmplusgvalb 21324 frlmup1 21353 islindf4 21393 mplind 21631 matgrp 21932 tlmtgp 23700 clmgrp 24584 ncvspi 24673 cphtcphnm 24747 ipcau2 24751 tcphcphlem1 24752 tcphcph 24754 rrxnm 24908 rrxds 24910 pjthlem2 24955 lmodvslmhm 32202 eqgvscpbl 32465 imaslmod 32468 quslmod 32469 linds2eq 32497 lbslsat 32701 lindsunlem 32709 lbsdiflsp0 32711 dimkerim 32712 lclkrlem2m 40390 mapdpglem14 40556 baerlem3lem1 40578 baerlem5amN 40587 baerlem5bmN 40588 baerlem5abmN 40589 mapdh6bN 40608 mapdh6cN 40609 hdmap1l6b 40682 hdmap1l6c 40683 hdmap11 40719 frlmsnic 41110 kercvrlsm 41825 pwssplit4 41831 pwslnmlem2 41835 mendring 41934 zlmodzxzsub 47036 lmodvsmdi 47058 lincvalsng 47097 lincvalsc0 47102 linc0scn0 47104 linc1 47106 lcoel0 47109 lindslinindimp2lem4 47142 snlindsntor 47152 lincresunit3 47162 |
Copyright terms: Public domain | W3C validator |