This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-assa

Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by SN, 2-Mar-2025)

Ref Expression
Assertion df-assa ⊢ AssAlg = w ∈ LMod ∩ Ring | [˙ Scalar ⁡ w / f]˙ ∀ r ∈ Base f ∀ x ∈ Base w ∀ y ∈ Base w [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y

Detailed syntax breakdown

Step Hyp Ref Expression
0 casa class AssAlg
1 vw setvar w
2 clmod class LMod
3 crg class Ring
4 2 3 cin class LMod ∩ Ring
5 csca class Scalar
6 1 cv setvar w
7 6 5 cfv class Scalar ⁡ w
8 vf setvar f
9 vr setvar r
10 cbs class Base
11 8 cv setvar f
12 11 10 cfv class Base f
13 vx setvar x
14 6 10 cfv class Base w
15 vy setvar y
16 cvsca class ⋅ 𝑠
17 6 16 cfv class ⋅ w
18 vs setvar s
19 cmulr class ⋅ 𝑟
20 6 19 cfv class ⋅ w
21 vt setvar t
22 9 cv setvar r
23 18 cv setvar s
24 13 cv setvar x
25 22 24 23 co class r s x
26 21 cv setvar t
27 15 cv setvar y
28 25 27 26 co class r s x t y
29 24 27 26 co class x t y
30 22 29 23 co class r s x t y
31 28 30 wceq wff r s x t y = r s x t y
32 22 27 23 co class r s y
33 24 32 26 co class x t r s y
34 33 30 wceq wff x t r s y = r s x t y
35 31 34 wa wff r s x t y = r s x t y ∧ x t r s y = r s x t y
36 35 21 20 wsbc wff [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y
37 36 18 17 wsbc wff [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y
38 37 15 14 wral wff ∀ y ∈ Base w [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y
39 38 13 14 wral wff ∀ x ∈ Base w ∀ y ∈ Base w [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y
40 39 9 12 wral wff ∀ r ∈ Base f ∀ x ∈ Base w ∀ y ∈ Base w [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y
41 40 8 7 wsbc wff [˙ Scalar ⁡ w / f]˙ ∀ r ∈ Base f ∀ x ∈ Base w ∀ y ∈ Base w [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y
42 41 1 4 crab class w ∈ LMod ∩ Ring | [˙ Scalar ⁡ w / f]˙ ∀ r ∈ Base f ∀ x ∈ Base w ∀ y ∈ Base w [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y
43 0 42 wceq wff AssAlg = w ∈ LMod ∩ Ring | [˙ Scalar ⁡ w / f]˙ ∀ r ∈ Base f ∀ x ∈ Base w ∀ y ∈ Base w [˙⋅ w / s]˙ [˙⋅ w / t]˙ r s x t y = r s x t y ∧ x t r s y = r s x t y