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

Definition df-sra 19375
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 19371 . 2 class subringAlg
2 vw . . 3 setvar 𝑤
3 cvv 3387 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1636 . . . . . 6 class 𝑤
6 cbs 16062 . . . . . 6 class Base
75, 6cfv 6095 . . . . 5 class (Base‘𝑤)
87cpw 4345 . . . 4 class 𝒫 (Base‘𝑤)
9 cnx 16059 . . . . . . . . 9 class ndx
10 csca 16150 . . . . . . . . 9 class Scalar
119, 10cfv 6095 . . . . . . . 8 class (Scalar‘ndx)
124cv 1636 . . . . . . . . 9 class 𝑠
13 cress 16063 . . . . . . . . 9 class s
145, 12, 13co 6868 . . . . . . . 8 class (𝑤s 𝑠)
1511, 14cop 4370 . . . . . . 7 class ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩
16 csts 16060 . . . . . . 7 class sSet
175, 15, 16co 6868 . . . . . 6 class (𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩)
18 cvsca 16151 . . . . . . . 8 class ·𝑠
199, 18cfv 6095 . . . . . . 7 class ( ·𝑠 ‘ndx)
20 cmulr 16148 . . . . . . . 8 class .r
215, 20cfv 6095 . . . . . . 7 class (.r𝑤)
2219, 21cop 4370 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩
2317, 22, 16co 6868 . . . . 5 class ((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩)
24 cip 16152 . . . . . . 7 class ·𝑖
259, 24cfv 6095 . . . . . 6 class (·𝑖‘ndx)
2625, 21cop 4370 . . . . 5 class ⟨(·𝑖‘ndx), (.r𝑤)⟩
2723, 26, 16co 6868 . . . 4 class (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)
284, 8, 27cmpt 4916 . . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩))
292, 3, 28cmpt 4916 . 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)))
301, 29wceq 1637 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  19379
  Copyright terms: Public domain W3C validator