# Metamath Proof Explorer

## Theorem asclmul1

Description: Left multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses asclmul1.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
asclmul1.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
asclmul1.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
asclmul1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
asclmul1.t
asclmul1.s
Assertion asclmul1

### Proof

Step Hyp Ref Expression
1 asclmul1.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 asclmul1.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 asclmul1.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
4 asclmul1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
5 asclmul1.t
6 asclmul1.s
7 eqid ${⊢}{1}_{{W}}={1}_{{W}}$
8 1 2 3 6 7 asclval
10 9 oveq1d
11 simp1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {X}\in {V}\right)\to {W}\in \mathrm{AssAlg}$
12 simp2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {X}\in {V}\right)\to {R}\in {K}$
13 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
14 13 3ad2ant1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {X}\in {V}\right)\to {W}\in \mathrm{Ring}$
15 4 7 ringidcl ${⊢}{W}\in \mathrm{Ring}\to {1}_{{W}}\in {V}$
16 14 15 syl ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {X}\in {V}\right)\to {1}_{{W}}\in {V}$
17 simp3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {X}\in {V}\right)\to {X}\in {V}$
18 4 2 3 6 5 assaass
19 11 12 16 17 18 syl13anc
20 4 5 7 ringlidm
21 14 17 20 syl2anc
22 21 oveq2d
23 10 19 22 3eqtrd