# Metamath Proof Explorer

## Theorem isassa

Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

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

### Proof

Step Hyp Ref Expression
1 isassa.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 isassa.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 isassa.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
4 isassa.s
5 isassa.t
6 fvexd ${⊢}{w}={W}\to \mathrm{Scalar}\left({w}\right)\in \mathrm{V}$
7 fveq2 ${⊢}{w}={W}\to \mathrm{Scalar}\left({w}\right)=\mathrm{Scalar}\left({W}\right)$
8 7 2 eqtr4di ${⊢}{w}={W}\to \mathrm{Scalar}\left({w}\right)={F}$
9 simpr ${⊢}\left({w}={W}\wedge {f}={F}\right)\to {f}={F}$
10 9 eleq1d ${⊢}\left({w}={W}\wedge {f}={F}\right)\to \left({f}\in \mathrm{CRing}↔{F}\in \mathrm{CRing}\right)$
11 9 fveq2d ${⊢}\left({w}={W}\wedge {f}={F}\right)\to {\mathrm{Base}}_{{f}}={\mathrm{Base}}_{{F}}$
12 11 3 eqtr4di ${⊢}\left({w}={W}\wedge {f}={F}\right)\to {\mathrm{Base}}_{{f}}={B}$
13 fveq2 ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={\mathrm{Base}}_{{W}}$
14 13 1 eqtr4di ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={V}$
15 fvexd ${⊢}{w}={W}\to {\cdot }_{{w}}\in \mathrm{V}$
16 fvexd ${⊢}\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\to {\cdot }_{{w}}\in \mathrm{V}$
17 simpr ${⊢}\left(\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\wedge {t}={\cdot }_{{w}}\right)\to {t}={\cdot }_{{w}}$
18 fveq2 ${⊢}{w}={W}\to {\cdot }_{{w}}={\cdot }_{{W}}$
19 18 ad2antrr ${⊢}\left(\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\wedge {t}={\cdot }_{{w}}\right)\to {\cdot }_{{w}}={\cdot }_{{W}}$
20 19 5 eqtr4di
21 17 20 eqtrd
22 simplr ${⊢}\left(\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\wedge {t}={\cdot }_{{w}}\right)\to {s}={\cdot }_{{w}}$
23 fveq2 ${⊢}{w}={W}\to {\cdot }_{{w}}={\cdot }_{{W}}$
24 23 ad2antrr ${⊢}\left(\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\wedge {t}={\cdot }_{{w}}\right)\to {\cdot }_{{w}}={\cdot }_{{W}}$
25 24 4 eqtr4di
26 22 25 eqtrd
27 26 oveqd
28 eqidd ${⊢}\left(\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\wedge {t}={\cdot }_{{w}}\right)\to {y}={y}$
29 21 27 28 oveq123d
30 eqidd ${⊢}\left(\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\wedge {t}={\cdot }_{{w}}\right)\to {r}={r}$
31 21 oveqd
32 26 30 31 oveq123d
33 29 32 eqeq12d
34 eqidd ${⊢}\left(\left({w}={W}\wedge {s}={\cdot }_{{w}}\right)\wedge {t}={\cdot }_{{w}}\right)\to {x}={x}$
35 26 oveqd
36 21 34 35 oveq123d
37 36 32 eqeq12d
38 33 37 anbi12d
39 16 38 sbcied
40 15 39 sbcied
41 14 40 raleqbidv
42 14 41 raleqbidv
50 elin ${⊢}{W}\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)↔\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\right)$
51 50 anbi1i ${⊢}\left({W}\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge {F}\in \mathrm{CRing}\right)↔\left(\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\right)\wedge {F}\in \mathrm{CRing}\right)$
52 df-3an ${⊢}\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {F}\in \mathrm{CRing}\right)↔\left(\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\right)\wedge {F}\in \mathrm{CRing}\right)$
53 51 52 bitr4i ${⊢}\left({W}\in \left(\mathrm{LMod}\cap \mathrm{Ring}\right)\wedge {F}\in \mathrm{CRing}\right)↔\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {F}\in \mathrm{CRing}\right)$