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 18939
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 18935 . 2 class subringAlg
2 vw . . 3 setvar 𝑤
3 cvv 3172 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1473 . . . . . 6 class 𝑤
6 cbs 15641 . . . . . 6 class Base
75, 6cfv 5790 . . . . 5 class (Base‘𝑤)
87cpw 4107 . . . 4 class 𝒫 (Base‘𝑤)
9 cnx 15638 . . . . . . . . 9 class ndx
10 csca 15717 . . . . . . . . 9 class Scalar
119, 10cfv 5790 . . . . . . . 8 class (Scalar‘ndx)
124cv 1473 . . . . . . . . 9 class 𝑠
13 cress 15642 . . . . . . . . 9 class s
145, 12, 13co 6527 . . . . . . . 8 class (𝑤s 𝑠)
1511, 14cop 4130 . . . . . . 7 class ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩
16 csts 15639 . . . . . . 7 class sSet
175, 15, 16co 6527 . . . . . 6 class (𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩)
18 cvsca 15718 . . . . . . . 8 class ·𝑠
199, 18cfv 5790 . . . . . . 7 class ( ·𝑠 ‘ndx)
20 cmulr 15715 . . . . . . . 8 class .r
215, 20cfv 5790 . . . . . . 7 class (.r𝑤)
2219, 21cop 4130 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩
2317, 22, 16co 6527 . . . . 5 class ((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩)
24 cip 15719 . . . . . . 7 class ·𝑖
259, 24cfv 5790 . . . . . 6 class (·𝑖‘ndx)
2625, 21cop 4130 . . . . 5 class ⟨(·𝑖‘ndx), (.r𝑤)⟩
2723, 26, 16co 6527 . . . 4 class (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)
284, 8, 27cmpt 4637 . . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩))
292, 3, 28cmpt 4637 . 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet ⟨(Scalar‘ndx), (𝑤s 𝑠)⟩) sSet ⟨( ·𝑠 ‘ndx), (.r𝑤)⟩) sSet ⟨(·𝑖‘ndx), (.r𝑤)⟩)))
301, 29wceq 1474 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  18943
  Copyright terms: Public domain W3C validator