Metamath Proof Explorer


Theorem lmodring

Description: The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypothesis lmodring.1 โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
Assertion lmodring ( ๐‘Š โˆˆ LMod โ†’ ๐น โˆˆ Ring )

Proof

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