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∈𝒫Basew⟼wsSetScalar⁡ndxw↾𝑠ssSet⋅ndx⋅wsSet⋅𝑖⁡ndx⋅w

Detailed syntax breakdown

Step Hyp Ref Expression
0 csra classsubringAlg
1 vw setvarw
2 cvv classV
3 vs setvars
4 cbs classBase
5 1 cv setvarw
6 5 4 cfv classBasew
7 6 cpw class𝒫Basew
8 csts classsSet
9 csca classScalar
10 cnx classndx
11 10 9 cfv classScalar⁡ndx
12 cress class↾𝑠
13 3 cv setvars
14 5 13 12 co classw↾𝑠s
15 11 14 cop classScalar⁡ndxw↾𝑠s
16 5 15 8 co classwsSetScalar⁡ndxw↾𝑠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 classwsSetScalar⁡ndxw↾𝑠ssSet⋅ndx⋅w
23 cip class⋅𝑖
24 10 23 cfv class⋅𝑖⁡ndx
25 24 20 cop class⋅𝑖⁡ndx⋅w
26 22 25 8 co classwsSetScalar⁡ndxw↾𝑠ssSet⋅ndx⋅wsSet⋅𝑖⁡ndx⋅w
27 3 7 26 cmpt classs∈𝒫Basew⟼wsSetScalar⁡ndxw↾𝑠ssSet⋅ndx⋅wsSet⋅𝑖⁡ndx⋅w
28 1 2 27 cmpt classw∈V⟼s∈𝒫Basew⟼wsSetScalar⁡ndxw↾𝑠ssSet⋅ndx⋅wsSet⋅𝑖⁡ndx⋅w
29 0 28 wceq wffsubringAlg=w∈V⟼s∈𝒫Basew⟼wsSetScalar⁡ndxw↾𝑠ssSet⋅ndx⋅wsSet⋅𝑖⁡ndx⋅w