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

Definition df-sra 16246
 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 sSet Scalar s sSet
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-sra
StepHypRef Expression
1 csra 16242 . 2 subringAlg
2 vw . . 3
3 cvv 2958 . . 3
4 vs . . . 4
52cv 1652 . . . . . 6
6 cbs 13471 . . . . . 6
75, 6cfv 5456 . . . . 5
87cpw 3801 . . . 4
9 cnx 13468 . . . . . . . 8
10 csca 13534 . . . . . . . 8 Scalar
119, 10cfv 5456 . . . . . . 7 Scalar
124cv 1652 . . . . . . . 8
13 cress 13472 . . . . . . . 8 s
145, 12, 13co 6083 . . . . . . 7 s
1511, 14cop 3819 . . . . . 6 Scalar s
16 csts 13469 . . . . . 6 sSet
175, 15, 16co 6083 . . . . 5 sSet Scalar s
18 cvsca 13535 . . . . . . 7
199, 18cfv 5456 . . . . . 6
20 cmulr 13532 . . . . . . 7
215, 20cfv 5456 . . . . . 6
2219, 21cop 3819 . . . . 5
2317, 22, 16co 6083 . . . 4 sSet Scalar s sSet
244, 8, 23cmpt 4268 . . 3 sSet Scalar s sSet
252, 3, 24cmpt 4268 . 2 sSet Scalar s sSet
261, 25wceq 1653 1 subringAlg sSet Scalar s sSet
 Colors of variables: wff set class This definition is referenced by:  sraval  16250
 Copyright terms: Public domain W3C validator