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

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

Detailed syntax breakdown of Definition df-sra
StepHypRef Expression
1 csra 17171 . 2  class subringAlg
2 vw . . 3  setvar  w
3 cvv 2962 . . 3  class  _V
4 vs . . . 4  setvar  s
52cv 1361 . . . . . 6  class  w
6 cbs 14157 . . . . . 6  class  Base
75, 6cfv 5406 . . . . 5  class  ( Base `  w )
87cpw 3848 . . . 4  class  ~P ( Base `  w )
9 cnx 14154 . . . . . . . . 9  class  ndx
10 csca 14224 . . . . . . . . 9  class Scalar
119, 10cfv 5406 . . . . . . . 8  class  (Scalar `  ndx )
124cv 1361 . . . . . . . . 9  class  s
13 cress 14158 . . . . . . . . 9  classs
145, 12, 13co 6080 . . . . . . . 8  class  ( ws  s )
1511, 14cop 3871 . . . . . . 7  class  <. (Scalar ` 
ndx ) ,  ( ws  s ) >.
16 csts 14155 . . . . . . 7  class sSet
175, 15, 16co 6080 . . . . . 6  class  ( w sSet  <. (Scalar `  ndx ) ,  ( ws  s ) >.
)
18 cvsca 14225 . . . . . . . 8  class  .s
199, 18cfv 5406 . . . . . . 7  class  ( .s
`  ndx )
20 cmulr 14222 . . . . . . . 8  class  .r
215, 20cfv 5406 . . . . . . 7  class  ( .r
`  w )
2219, 21cop 3871 . . . . . 6  class  <. ( .s `  ndx ) ,  ( .r `  w
) >.
2317, 22, 16co 6080 . . . . 5  class  ( ( w sSet  <. (Scalar `  ndx ) ,  ( ws  s
) >. ) sSet  <. ( .s `  ndx ) ,  ( .r `  w
) >. )
24 cip 14226 . . . . . . 7  class  .i
259, 24cfv 5406 . . . . . 6  class  ( .i
`  ndx )
2625, 21cop 3871 . . . . 5  class  <. ( .i `  ndx ) ,  ( .r `  w
) >.
2723, 26, 16co 6080 . . . 4  class  ( ( ( w sSet  <. (Scalar ` 
ndx ) ,  ( ws  s ) >. ) sSet  <.
( .s `  ndx ) ,  ( .r `  w ) >. ) sSet  <.
( .i `  ndx ) ,  ( .r `  w ) >. )
284, 8, 27cmpt 4338 . . 3  class  ( s  e.  ~P ( Base `  w )  |->  ( ( ( w sSet  <. (Scalar ` 
ndx ) ,  ( ws  s ) >. ) sSet  <.
( .s `  ndx ) ,  ( .r `  w ) >. ) sSet  <.
( .i `  ndx ) ,  ( .r `  w ) >. )
)
292, 3, 28cmpt 4338 . 2  class  ( w  e.  _V  |->  ( s  e.  ~P ( Base `  w )  |->  ( ( ( w sSet  <. (Scalar ` 
ndx ) ,  ( ws  s ) >. ) sSet  <.
( .s `  ndx ) ,  ( .r `  w ) >. ) sSet  <.
( .i `  ndx ) ,  ( .r `  w ) >. )
) )
301, 29wceq 1362 1  wff subringAlg  =  ( w  e.  _V  |->  ( s  e.  ~P ( Base `  w )  |->  ( ( ( w sSet  <. (Scalar `  ndx ) ,  ( ws  s ) >. ) sSet  <.
( .s `  ndx ) ,  ( .r `  w ) >. ) sSet  <.
( .i `  ndx ) ,  ( .r `  w ) >. )
) )
Colors of variables: wff setvar class
This definition is referenced by:  sraval  17179
  Copyright terms: Public domain W3C validator