Metamath Proof Explorer

Definition df-lmod

Description: Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013)

Ref Expression
Assertion df-lmod LMod = { 𝑔 ∈ Grp ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmod ⊢ LMod
1 vg ⊢ 𝑔
2 cgrp ⊢ Grp
3 cbs ⊢ Base
4 1 cv ⊢ 𝑔
5 4 3 cfv ⊢ ( Base ‘ 𝑔 )
6 vv ⊢ 𝑣
7 cplusg ⊢ +g
8 4 7 cfv ⊢ ( +g ‘ 𝑔 )
9 va ⊢ 𝑎
10 csca ⊢ Scalar
11 4 10 cfv ⊢ ( Scalar ‘ 𝑔 )
12 vf ⊢ 𝑓
13 cvsca ⊢ ·𝑠
14 4 13 cfv ⊢ ( ·𝑠 ‘ 𝑔 )
15 vs ⊢ 𝑠
16 12 cv ⊢ 𝑓
17 16 3 cfv ⊢ ( Base ‘ 𝑓 )
18 vk ⊢ 𝑘
19 16 7 cfv ⊢ ( +g ‘ 𝑓 )
20 vp ⊢ 𝑝
21 cmulr ⊢ .r
22 16 21 cfv ⊢ ( .r ‘ 𝑓 )
23 vt ⊢ 𝑡
24 crg ⊢ Ring
25 16 24 wcel ⊢ 𝑓 ∈ Ring
26 vq ⊢ 𝑞
27 18 cv ⊢ 𝑘
28 vr ⊢ 𝑟
29 vx ⊢ 𝑥
30 6 cv ⊢ 𝑣
31 vw ⊢ 𝑤
32 28 cv ⊢ 𝑟
33 15 cv ⊢ 𝑠
34 31 cv ⊢ 𝑤
35 32 34 33 co ⊢ ( 𝑟 𝑠 𝑤 )
36 35 30 wcel ⊢ ( 𝑟 𝑠 𝑤 ) ∈ 𝑣
37 9 cv ⊢ 𝑎
38 29 cv ⊢ 𝑥
39 34 38 37 co ⊢ ( 𝑤 𝑎 𝑥 )
40 32 39 33 co ⊢ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) )
41 32 38 33 co ⊢ ( 𝑟 𝑠 𝑥 )
42 35 41 37 co ⊢ ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) )
43 40 42 wceq ⊢ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) )
44 26 cv ⊢ 𝑞
45 20 cv ⊢ 𝑝
46 44 32 45 co ⊢ ( 𝑞 𝑝 𝑟 )
47 46 34 33 co ⊢ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 )
48 44 34 33 co ⊢ ( 𝑞 𝑠 𝑤 )
49 48 35 37 co ⊢ ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) )
50 47 49 wceq ⊢ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) )
51 36 43 50 w3a ⊢ ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) )
52 23 cv ⊢ 𝑡
53 44 32 52 co ⊢ ( 𝑞 𝑡 𝑟 )
54 53 34 33 co ⊢ ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 )
55 44 35 33 co ⊢ ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) )
56 54 55 wceq ⊢ ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) )
57 cur ⊢ 1r
58 16 57 cfv ⊢ ( 1r ‘ 𝑓 )
59 58 34 33 co ⊢ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 )
60 59 34 wceq ⊢ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤
61 56 60 wa ⊢ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 )
62 51 61 wa ⊢ ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) )
63 62 31 30 wral ⊢ ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) )
64 63 29 30 wral ⊢ ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) )
65 64 28 27 wral ⊢ ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) )
66 65 26 27 wral ⊢ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) )
67 25 66 wa ⊢ ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
68 67 23 22 wsbc ⊢ [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
69 68 20 19 wsbc ⊢ [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
70 69 18 17 wsbc ⊢ [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
71 70 15 14 wsbc ⊢ [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
72 71 12 11 wsbc ⊢ [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
73 72 9 8 wsbc ⊢ [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
74 73 6 5 wsbc ⊢ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) )
75 74 1 2 crab ⊢ { 𝑔 ∈ Grp ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) }
76 0 75 wceq ⊢ LMod = { 𝑔 ∈ Grp ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ Ring ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ) ) ) }