Definition df-sra 20778

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.)

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 20774	. 2 class subringAlg
2		vw	. . 3 setvar 𝑤
3		cvv 3475	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1541	. . . . . 6 class 𝑤
6		cbs 17141	. . . . . 6 class Base
7	5, 6	cfv 6541	. . . . 5 class (Base‘𝑤)
8	7	cpw 4602	. . . 4 class 𝒫 (Base‘𝑤)
9		cnx 17123	. . . . . . . . 9 class ndx
10		csca 17197	. . . . . . . . 9 class Scalar
11	9, 10	cfv 6541	. . . . . . . 8 class (Scalar‘ndx)
12	4	cv 1541	. . . . . . . . 9 class 𝑠
13		cress 17170	. . . . . . . . 9 class ↾s
14	5, 12, 13	co 7406	. . . . . . . 8 class (𝑤 ↾s 𝑠)
15	11, 14	cop 4634	. . . . . . 7 class ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩
16		csts 17093	. . . . . . 7 class sSet
17	5, 15, 16	co 7406	. . . . . 6 class (𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩)
18		cvsca 17198	. . . . . . . 8 class ·𝑠
19	9, 18	cfv 6541	. . . . . . 7 class ( ·𝑠 ‘ndx)
20		cmulr 17195	. . . . . . . 8 class .r
21	5, 20	cfv 6541	. . . . . . 7 class (.r‘𝑤)
22	19, 21	cop 4634	. . . . . 6 class ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩
23	17, 22, 16	co 7406	. . . . 5 class ((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩)
24		cip 17199	. . . . . . 7 class ·𝑖
25	9, 24	cfv 6541	. . . . . 6 class (·𝑖‘ndx)
26	25, 21	cop 4634	. . . . 5 class ⟨(·𝑖‘ndx), (.r‘𝑤)⟩
27	23, 26, 16	co 7406	. . . 4 class (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)
28	4, 8, 27	cmpt 5231	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩))
29	2, 3, 28	cmpt 5231	. 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)))
30	1, 29	wceq 1542	1 wff subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤 ↾s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r‘𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r‘𝑤)⟩)))

This definition is referenced by:  sraval  20782