# Metamath Proof Explorer

## Theorem assamulgscmlem1

Description: Lemma 1 for assamulgscm (induction base). (Contributed by AV, 26-Aug-2019)

Ref Expression
Hypotheses assamulgscm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
assamulgscm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
assamulgscm.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
assamulgscm.s
assamulgscm.g ${⊢}{G}={\mathrm{mulGrp}}_{{F}}$
assamulgscm.p
assamulgscm.h ${⊢}{H}={\mathrm{mulGrp}}_{{W}}$
assamulgscm.e ${⊢}{E}={\cdot }_{{H}}$
Assertion assamulgscmlem1

### Proof

Step Hyp Ref Expression
1 assamulgscm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 assamulgscm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 assamulgscm.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
4 assamulgscm.s
5 assamulgscm.g ${⊢}{G}={\mathrm{mulGrp}}_{{F}}$
6 assamulgscm.p
7 assamulgscm.h ${⊢}{H}={\mathrm{mulGrp}}_{{W}}$
8 assamulgscm.e ${⊢}{E}={\cdot }_{{H}}$
9 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
10 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
11 eqid ${⊢}{1}_{{W}}={1}_{{W}}$
12 1 11 ringidcl ${⊢}{W}\in \mathrm{Ring}\to {1}_{{W}}\in {V}$
13 10 12 syl ${⊢}{W}\in \mathrm{AssAlg}\to {1}_{{W}}\in {V}$
14 eqid ${⊢}{1}_{{F}}={1}_{{F}}$
15 1 2 4 14 lmodvs1
16 15 eqcomd
17 9 13 16 syl2anc
19 9 adantl ${⊢}\left(\left({A}\in {B}\wedge {X}\in {V}\right)\wedge {W}\in \mathrm{AssAlg}\right)\to {W}\in \mathrm{LMod}$
20 simpll ${⊢}\left(\left({A}\in {B}\wedge {X}\in {V}\right)\wedge {W}\in \mathrm{AssAlg}\right)\to {A}\in {B}$
21 simplr ${⊢}\left(\left({A}\in {B}\wedge {X}\in {V}\right)\wedge {W}\in \mathrm{AssAlg}\right)\to {X}\in {V}$
22 1 2 4 3 lmodvscl
23 19 20 21 22 syl3anc
24 7 1 mgpbas ${⊢}{V}={\mathrm{Base}}_{{H}}$
25 7 11 ringidval ${⊢}{1}_{{W}}={0}_{{H}}$
26 24 25 8 mulg0
27 23 26 syl
28 5 3 mgpbas ${⊢}{B}={\mathrm{Base}}_{{G}}$
29 5 14 ringidval ${⊢}{1}_{{F}}={0}_{{G}}$
30 28 29 6 mulg0
31 20 30 syl
32 24 25 8 mulg0 ${⊢}{X}\in {V}\to 0{E}{X}={1}_{{W}}$
33 21 32 syl ${⊢}\left(\left({A}\in {B}\wedge {X}\in {V}\right)\wedge {W}\in \mathrm{AssAlg}\right)\to 0{E}{X}={1}_{{W}}$
34 31 33 oveq12d
35 18 27 34 3eqtr4d