Metamath Proof Explorer


Theorem lmodgrp

Description: A left module is a group. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 25-Jun-2014)

Ref Expression
Assertion lmodgrp ( ๐‘Š โˆˆ LMod โ†’ ๐‘Š โˆˆ Grp )

Proof

Step Hyp Ref Expression
1 eqid โŠข ( Base โ€˜ ๐‘Š ) = ( Base โ€˜ ๐‘Š )
2 eqid โŠข ( +g โ€˜ ๐‘Š ) = ( +g โ€˜ ๐‘Š )
3 eqid โŠข ( ยท๐‘  โ€˜ ๐‘Š ) = ( ยท๐‘  โ€˜ ๐‘Š )
4 eqid โŠข ( Scalar โ€˜ ๐‘Š ) = ( Scalar โ€˜ ๐‘Š )
5 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) )
6 eqid โŠข ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) )
7 eqid โŠข ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) )
8 eqid โŠข ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) )
9 1 2 3 4 5 6 7 8 islmod โŠข ( ๐‘Š โˆˆ LMod โ†” ( ๐‘Š โˆˆ Grp โˆง ( Scalar โ€˜ ๐‘Š ) โˆˆ Ring โˆง โˆ€ ๐‘ž โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆ€ ๐‘Ÿ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘Š ) ) โˆ€ ๐‘ฅ โˆˆ ( Base โ€˜ ๐‘Š ) โˆ€ ๐‘ค โˆˆ ( Base โ€˜ ๐‘Š ) ( ( ( ๐‘Ÿ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) โˆˆ ( Base โ€˜ ๐‘Š ) โˆง ( ๐‘Ÿ ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘ค ( +g โ€˜ ๐‘Š ) ๐‘ฅ ) ) = ( ( ๐‘Ÿ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ÿ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ฅ ) ) โˆง ( ( ๐‘ž ( +g โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ๐‘Ÿ ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) = ( ( ๐‘ž ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) ( +g โ€˜ ๐‘Š ) ( ๐‘Ÿ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) ) ) โˆง ( ( ( ๐‘ž ( .r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ๐‘Ÿ ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) = ( ๐‘ž ( ยท๐‘  โ€˜ ๐‘Š ) ( ๐‘Ÿ ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) ) โˆง ( ( 1r โ€˜ ( Scalar โ€˜ ๐‘Š ) ) ( ยท๐‘  โ€˜ ๐‘Š ) ๐‘ค ) = ๐‘ค ) ) ) )
10 9 simp1bi โŠข ( ๐‘Š โˆˆ LMod โ†’ ๐‘Š โˆˆ Grp )