# Metamath Proof Explorer

## Theorem assa2ass

Description: Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019)

Ref Expression
Hypotheses assa2ass.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
assa2ass.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
assa2ass.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
assa2ass.m
assa2ass.s
assa2ass.t
Assertion assa2ass

### Proof

Step Hyp Ref Expression
1 assa2ass.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 assa2ass.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 assa2ass.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
4 assa2ass.m
5 assa2ass.s
6 assa2ass.t
7 simp1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {W}\in \mathrm{AssAlg}$
8 simpr ${⊢}\left({A}\in {B}\wedge {C}\in {B}\right)\to {C}\in {B}$
9 8 3ad2ant2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {C}\in {B}$
10 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
11 simpl ${⊢}\left({A}\in {B}\wedge {C}\in {B}\right)\to {A}\in {B}$
12 simpl ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to {X}\in {V}$
13 1 2 5 3 lmodvscl
14 10 11 12 13 syl3an
15 simpr ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to {Y}\in {V}$
16 15 3ad2ant3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {Y}\in {V}$
17 1 2 3 5 6 assaassr
18 7 9 14 16 17 syl13anc
19 1 2 3 5 6 assaass
20 19 eqcomd
21 7 9 14 16 20 syl13anc
22 10 3ad2ant1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {W}\in \mathrm{LMod}$
23 11 3ad2ant2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {A}\in {B}$
24 12 3ad2ant3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\wedge \left({X}\in {V}\wedge {Y}\in {V}\right)\right)\to {X}\in {V}$
25 1 2 5 3 4 lmodvsass
26 25 eqcomd
27 26 oveq1d
28 22 9 23 24 27 syl13anc
29 2 assasca ${⊢}{W}\in \mathrm{AssAlg}\to {F}\in \mathrm{CRing}$
30 crngring ${⊢}{F}\in \mathrm{CRing}\to {F}\in \mathrm{Ring}$
31 29 30 syl ${⊢}{W}\in \mathrm{AssAlg}\to {F}\in \mathrm{Ring}$
32 31 adantr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\right)\to {F}\in \mathrm{Ring}$
33 8 adantl ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\right)\to {C}\in {B}$
34 11 adantl ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in {B}\wedge {C}\in {B}\right)\right)\to {A}\in {B}$
35 3 4 ringcl
36 32 33 34 35 syl3anc