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 = { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ∀ 𝑟 ∈ ( 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		vr	⊢ 𝑟
10		cbs	⊢ Base
11	8	cv	⊢ 𝑓
12	11 10	cfv	⊢ ( Base ‘ 𝑓 )
13		vx	⊢ 𝑥
14	6 10	cfv	⊢ ( Base ‘ 𝑤 )
15		vy	⊢ 𝑦
16		cvsca	⊢ ·𝑠
17	6 16	cfv	⊢ ( ·𝑠 ‘ 𝑤 )
18		vs	⊢ 𝑠
19		cmulr	⊢ .r
20	6 19	cfv	⊢ ( .r ‘ 𝑤 )
21		vt	⊢ 𝑡
22	9	cv	⊢ 𝑟
23	18	cv	⊢ 𝑠
24	13	cv	⊢ 𝑥
25	22 24 23	co	⊢ ( 𝑟 𝑠 𝑥 )
26	21	cv	⊢ 𝑡
27	15	cv	⊢ 𝑦
28	25 27 26	co	⊢ ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 )
29	24 27 26	co	⊢ ( 𝑥 𝑡 𝑦 )
30	22 29 23	co	⊢ ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) )
31	28 30	wceq	⊢ ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) )
32	22 27 23	co	⊢ ( 𝑟 𝑠 𝑦 )
33	24 32 26	co	⊢ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) )
34	33 30	wceq	⊢ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) )
35	31 34	wa	⊢ ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
36	35 21 20	wsbc	⊢ [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
37	36 18 17	wsbc	⊢ [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
38	37 15 14	wral	⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
39	38 13 14	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
40	39 9 12	wral	⊢ ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
41	40 8 7	wsbc	⊢ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) )
42	41 1 4	crab	⊢ { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) }
43	0 42	wceq	⊢ AssAlg = { 𝑤 ∈ ( LMod ∩ Ring ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ∀ 𝑟 ∈ ( Base ‘ 𝑓 ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) [ ( ·𝑠 ‘ 𝑤 ) / 𝑠 ] [ ( .r ‘ 𝑤 ) / 𝑡 ] ( ( ( 𝑟 𝑠 𝑥 ) 𝑡 𝑦 ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ∧ ( 𝑥 𝑡 ( 𝑟 𝑠 𝑦 ) ) = ( 𝑟 𝑠 ( 𝑥 𝑡 𝑦 ) ) ) }