# Metamath Proof Explorer

## Theorem ascl0

Description: The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019)

Ref Expression
Hypotheses ascl0.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
ascl0.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
ascl0.l ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
ascl0.r ${⊢}{\phi }\to {W}\in \mathrm{Ring}$
Assertion ascl0 ${⊢}{\phi }\to {A}\left({0}_{{F}}\right)={0}_{{W}}$

### Proof

Step Hyp Ref Expression
1 ascl0.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 ascl0.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 ascl0.l ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
4 ascl0.r ${⊢}{\phi }\to {W}\in \mathrm{Ring}$
5 2 lmodfgrp ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Grp}$
6 3 5 syl ${⊢}{\phi }\to {F}\in \mathrm{Grp}$
7 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
8 eqid ${⊢}{0}_{{F}}={0}_{{F}}$
9 7 8 grpidcl ${⊢}{F}\in \mathrm{Grp}\to {0}_{{F}}\in {\mathrm{Base}}_{{F}}$
10 6 9 syl ${⊢}{\phi }\to {0}_{{F}}\in {\mathrm{Base}}_{{F}}$
11 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
12 eqid ${⊢}{1}_{{W}}={1}_{{W}}$
13 1 2 7 11 12 asclval ${⊢}{0}_{{F}}\in {\mathrm{Base}}_{{F}}\to {A}\left({0}_{{F}}\right)={0}_{{F}}{\cdot }_{{W}}{1}_{{W}}$
14 10 13 syl ${⊢}{\phi }\to {A}\left({0}_{{F}}\right)={0}_{{F}}{\cdot }_{{W}}{1}_{{W}}$
15 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
16 15 12 ringidcl ${⊢}{W}\in \mathrm{Ring}\to {1}_{{W}}\in {\mathrm{Base}}_{{W}}$
17 4 16 syl ${⊢}{\phi }\to {1}_{{W}}\in {\mathrm{Base}}_{{W}}$
18 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
19 15 2 11 8 18 lmod0vs ${⊢}\left({W}\in \mathrm{LMod}\wedge {1}_{{W}}\in {\mathrm{Base}}_{{W}}\right)\to {0}_{{F}}{\cdot }_{{W}}{1}_{{W}}={0}_{{W}}$
20 3 17 19 syl2anc ${⊢}{\phi }\to {0}_{{F}}{\cdot }_{{W}}{1}_{{W}}={0}_{{W}}$
21 14 20 eqtrd ${⊢}{\phi }\to {A}\left({0}_{{F}}\right)={0}_{{W}}$