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 = algSc W
ascl0.f F = Scalar W
ascl0.l φ W LMod
ascl0.r φ W Ring
Assertion ascl0 φ A 0 F = 0 W

Proof

Step Hyp Ref Expression
1 ascl0.a A = algSc W
2 ascl0.f F = Scalar W
3 ascl0.l φ W LMod
4 ascl0.r φ W Ring
5 2 lmodfgrp W LMod F Grp
6 eqid Base F = Base F
7 eqid 0 F = 0 F
8 6 7 grpidcl F Grp 0 F Base F
9 eqid W = W
10 eqid 1 W = 1 W
11 1 2 6 9 10 asclval 0 F Base F A 0 F = 0 F W 1 W
12 3 5 8 11 4syl φ A 0 F = 0 F W 1 W
13 eqid Base W = Base W
14 13 10 ringidcl W Ring 1 W Base W
15 4 14 syl φ 1 W Base W
16 eqid 0 W = 0 W
17 13 2 9 7 16 lmod0vs W LMod 1 W Base W 0 F W 1 W = 0 W
18 3 15 17 syl2anc φ 0 F W 1 W = 0 W
19 12 18 eqtrd φ A 0 F = 0 W