Metamath Proof Explorer

Definition df-sra

Description: Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (Contributed by Mario Carneiro, 27-Nov-2014) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Assertion df-sra ⊢ subringAlg = w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 csra class subringAlg
1 vw setvar w
2 cvv class V
3 vs setvar s
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 csts class sSet
9 csca class Scalar
10 cnx class ndx
11 10 9 cfv class Scalar ⁡ ndx
12 cress class ↾ 𝑠
13 3 cv setvar s
14 5 13 12 co class w ↾ 𝑠 s
15 11 14 cop class Scalar ⁡ ndx w ↾ 𝑠 s
16 5 15 8 co class w sSet Scalar ⁡ ndx w ↾ 𝑠 s
17 cvsca class ⋅ 𝑠
18 10 17 cfv class ⋅ ndx
19 cmulr class ⋅ 𝑟
20 5 19 cfv class ⋅ w
21 18 20 cop class ⋅ ndx ⋅ w
22 16 21 8 co class w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w
23 cip class ⋅ 𝑖
24 10 23 cfv class ⋅ 𝑖 ⁡ ndx
25 24 20 cop class ⋅ 𝑖 ⁡ ndx ⋅ w
26 22 25 8 co class w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w
27 3 7 26 cmpt class s ∈ 𝒫 Base w ⟼ w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w
28 1 2 27 cmpt class w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w
29 0 28 wceq wff subringAlg = w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w