Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sra Structured version   Visualization version   GIF version

Definition df-sra 19220
 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
StepHypRef Expression
1 csra 19216 . 2 class subringAlg
2 vw . . 3 setvar 𝑤
3 cvv 3231 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1522 . . . . . 6 class 𝑤
6 cbs 15904 . . . . . 6 class Base
75, 6cfv 5926 . . . . 5 class (Base‘𝑤)
87cpw 4191 . . . 4 class 𝒫 (Base‘𝑤)
9 cnx 15901 . . . . . . . . 9 class ndx
10 csca 15991 . . . . . . . . 9 class Scalar
119, 10cfv 5926 . . . . . . . 8 class (Scalar‘ndx)
124cv 1522 . . . . . . . . 9 class 𝑠
13 cress 15905 . . . . . . . . 9 class s
145, 12, 13co 6690 . . . . . . . 8 class (𝑤s 𝑠)
1511, 14cop 4216 . . . . . . 7 class ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩
16 csts 15902 . . . . . . 7 class sSet
175, 15, 16co 6690 . . . . . 6 class (𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩)
18 cvsca 15992 . . . . . . . 8 class ·𝑠
199, 18cfv 5926 . . . . . . 7 class ( ·𝑠 ‘ndx)
20 cmulr 15989 . . . . . . . 8 class .r
215, 20cfv 5926 . . . . . . 7 class (.r𝑤)
2219, 21cop 4216 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩
2317, 22, 16co 6690 . . . . 5 class ((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩)
24 cip 15993 . . . . . . 7 class ·𝑖
259, 24cfv 5926 . . . . . 6 class (·𝑖‘ndx)
2625, 21cop 4216 . . . . 5 class ⟨(·𝑖‘ndx), (.r𝑤)⟩
2723, 26, 16co 6690 . . . 4 class (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)
284, 8, 27cmpt 4762 . . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩))
292, 3, 28cmpt 4762 . 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)))
301, 29wceq 1523 1 wff subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)))
 Colors of variables: wff setvar class This definition is referenced by:  sraval  19224
 Copyright terms: Public domain W3C validator