Definition df-sra 18993

Description: Given any subring of a ring, we can construct a left-algebra by regarding the elements of the subring as scalars and the ring itself as a set of vectors. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)

Assertion

Ref	Expression
df-sra	⊢ subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)))

Distinct variable group:   𝑤,𝑠

Detailed syntax breakdown of Definition df-sra

Step	Hyp	Ref	Expression
1		csra 18989	. 2 class subringAlg
2		vw	. . 3 setvar 𝑤
3		cvv 3173	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1474	. . . . . 6 class 𝑤
6		cbs 15695	. . . . . 6 class Base
7	5, 6	cfv 5804	. . . . 5 class (Base‘𝑤)
8	7	cpw 4108	. . . 4 class 𝒫 (Base‘𝑤)
9		cnx 15692	. . . . . . . . 9 class ndx
10		csca 15771	. . . . . . . . 9 class Scalar
11	9, 10	cfv 5804	. . . . . . . 8 class (Scalar‘ndx)
12	4	cv 1474	. . . . . . . . 9 class 𝑠
13		cress 15696	. . . . . . . . 9 class ↾s
14	5, 12, 13	co 6549	. . . . . . . 8 class (𝑤 ↾s 𝑠)
15	11, 14	cop 4131	. . . . . . 7 class ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩
16		csts 15693	. . . . . . 7 class sSet
17	5, 15, 16	co 6549	. . . . . 6 class (𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩)
18		cvsca 15772	. . . . . . . 8 class ·𝑠
19	9, 18	cfv 5804	. . . . . . 7 class ( ·𝑠 ‘ndx)
20		cmulr 15769	. . . . . . . 8 class .r
21	5, 20	cfv 5804	. . . . . . 7 class (.r‘𝑤)
22	19, 21	cop 4131	. . . . . 6 class ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩
23	17, 22, 16	co 6549	. . . . 5 class ((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩)
24		cip 15773	. . . . . . 7 class ·𝑖
25	9, 24	cfv 5804	. . . . . 6 class (·𝑖‘ndx)
26	25, 21	cop 4131	. . . . 5 class ⟨(·𝑖‘ndx), (.r‘𝑤)⟩
27	23, 26, 16	co 6549	. . . 4 class (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)
28	4, 8, 27	cmpt 4643	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩))
29	2, 3, 28	cmpt 4643	. 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)))
30	1, 29	wceq 1475	1 wff subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)))

This definition is referenced by:  sraval  18997