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

Definition df-sra 15941
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.)
Assertion
Ref Expression
df-sra  |- subringAlg  =  ( w  e.  _V  |->  ( s  e.  ~P ( Base `  w )  |->  ( ( w sSet  <. (Scalar ` 
ndx ) ,  ( ws  s ) >. ) sSet  <.
( .s `  ndx ) ,  ( .r `  w ) >. )
) )
Distinct variable group:    w, s

Detailed syntax breakdown of Definition df-sra
StepHypRef Expression
1 csra 15937 . 2  class subringAlg
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
4 vs . . . 4  set  s
52cv 1631 . . . . . 6  class  w
6 cbs 13164 . . . . . 6  class  Base
75, 6cfv 5271 . . . . 5  class  ( Base `  w )
87cpw 3638 . . . 4  class  ~P ( Base `  w )
9 cnx 13161 . . . . . . . 8  class  ndx
10 csca 13227 . . . . . . . 8  class Scalar
119, 10cfv 5271 . . . . . . 7  class  (Scalar `  ndx )
124cv 1631 . . . . . . . 8  class  s
13 cress 13165 . . . . . . . 8  classs
145, 12, 13co 5874 . . . . . . 7  class  ( ws  s )
1511, 14cop 3656 . . . . . 6  class  <. (Scalar ` 
ndx ) ,  ( ws  s ) >.
16 csts 13162 . . . . . 6  class sSet
175, 15, 16co 5874 . . . . 5  class  ( w sSet  <. (Scalar `  ndx ) ,  ( ws  s ) >.
)
18 cvsca 13228 . . . . . . 7  class  .s
199, 18cfv 5271 . . . . . 6  class  ( .s
`  ndx )
20 cmulr 13225 . . . . . . 7  class  .r
215, 20cfv 5271 . . . . . 6  class  ( .r
`  w )
2219, 21cop 3656 . . . . 5  class  <. ( .s `  ndx ) ,  ( .r `  w
) >.
2317, 22, 16co 5874 . . . 4  class  ( ( w sSet  <. (Scalar `  ndx ) ,  ( ws  s
) >. ) sSet  <. ( .s `  ndx ) ,  ( .r `  w
) >. )
244, 8, 23cmpt 4093 . . 3  class  ( s  e.  ~P ( Base `  w )  |->  ( ( w sSet  <. (Scalar `  ndx ) ,  ( ws  s
) >. ) sSet  <. ( .s `  ndx ) ,  ( .r `  w
) >. ) )
252, 3, 24cmpt 4093 . 2  class  ( w  e.  _V  |->  ( s  e.  ~P ( Base `  w )  |->  ( ( w sSet  <. (Scalar `  ndx ) ,  ( ws  s
) >. ) sSet  <. ( .s `  ndx ) ,  ( .r `  w
) >. ) ) )
261, 25wceq 1632 1  wff subringAlg  =  ( w  e.  _V  |->  ( s  e.  ~P ( Base `  w )  |->  ( ( w sSet  <. (Scalar ` 
ndx ) ,  ( ws  s ) >. ) sSet  <.
( .s `  ndx ) ,  ( .r `  w ) >. )
) )
Colors of variables: wff set class
This definition is referenced by:  sraval  15945
  Copyright terms: Public domain W3C validator