Definition df-assa

Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) 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)

	Ref	Expression
Assertion	df-assa	⊢ AssAlg = { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		casa	⊢ AssAlg
1		vw	⊢ 𝑤
2		clmod	⊢ LMod
3		crg	⊢ Ring
4	2 3	cin	⊢ ( LMod ∩ Ring )
5		csca	⊢ Scalar
6	1	cv	⊢ 𝑤
7	6 5	cfv	⊢ ( Scalar ‘ 𝑤 )
8		vf	⊢ 𝑓
9	8	cv	⊢ 𝑓
10		ccrg	⊢ CRing
11	9 10	wcel	⊢ 𝑓 ∈ CRing
12		vr	⊢ 𝑟
13		cbs	⊢ Base
14	9 13	cfv	⊢ ( Base ‘ 𝑓 )
15		vx	⊢ 𝑥
16	6 13	cfv	⊢ ( Base ‘ 𝑤 )
17		vy	⊢ 𝑦
18		cvsca	⊢ ·𝑠
19	6 18	cfv	⊢ ( ·𝑠 ‘ 𝑤 )
20		vs	⊢ 𝑠
21		cmulr	⊢ .r
22	6 21	cfv	⊢ ( .r ‘ 𝑤 )
23		vt	⊢ 𝑡
24	12	cv	⊢ 𝑟
25	20	cv	⊢ 𝑠
26	15	cv	⊢ 𝑥
27	24 26 25	co	⊢ ( 𝑟 𝑠 𝑥 )
28	23	cv	⊢ 𝑡
29	17	cv	⊢ 𝑦
30	27 29 28	co	⊢ ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 )
31	26 29 28	co	⊢ ( 𝑥 𝑡 𝑦 )
32	24 31 25	co	⊢ ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) )
33	30 32	wceq	⊢ ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) )
34	24 29 25	co	⊢ ( 𝑟 𝑠 𝑦 )
35	26 34 28	co	⊢ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) )
36	35 32	wceq	⊢ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) )
37	33 36	wa	⊢ ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
38	37 23 22	wsbc	⊢ [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
39	38 20 19	wsbc	⊢ [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
40	39 17 16	wral	⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
41	40 15 16	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
42	41 12 14	wral	⊢ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
43	11 42	wa	⊢ ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) )
44	43 8 7	wsbc	⊢ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) )
45	44 1 4	crab	⊢ { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ) }
46	0 45	wceq	⊢ AssAlg = { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( 𝑓 ∈ CRing ∧ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) ) }