Definition df-sra 16199

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 ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) ) )

Distinct variable group:   w, s

Detailed syntax breakdown of Definition df-sra

Step	Hyp	Ref	Expression
1		csra 16195	. 2 class subringAlg
2		vw	. . 3 set w
3		cvv 2916	. . 3 class _V
4		vs	. . . 4 set s
5	2	cv 1648	. . . . . 6 class w
6		cbs 13424	. . . . . 6 class Base
7	5, 6	cfv 5413	. . . . 5 class ( Base ` w )
8	7	cpw 3759	. . . 4 class ~P ( Base ` w )
9		cnx 13421	. . . . . . . 8 class ndx
10		csca 13487	. . . . . . . 8 class Scalar
11	9, 10	cfv 5413	. . . . . . 7 class (Scalar ` ndx )
12	4	cv 1648	. . . . . . . 8 class s
13		cress 13425	. . . . . . . 8 class ↾s
14	5, 12, 13	co 6040	. . . . . . 7 class ( w ↾s s )
15	11, 14	cop 3777	. . . . . 6 class <. (Scalar ` ndx ) , ( w ↾s s ) >.
16		csts 13422	. . . . . 6 class sSet
17	5, 15, 16	co 6040	. . . . 5 class ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. )
18		cvsca 13488	. . . . . . 7 class .s
19	9, 18	cfv 5413	. . . . . 6 class ( .s ` ndx )
20		cmulr 13485	. . . . . . 7 class .r
21	5, 20	cfv 5413	. . . . . 6 class ( .r ` w )
22	19, 21	cop 3777	. . . . 5 class <. ( .s ` ndx ) , ( .r ` w ) >.
23	17, 22, 16	co 6040	. . . 4 class ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. )
24	4, 8, 23	cmpt 4226	. . 3 class ( s e. ~P ( Base ` w ) |-> ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) )
25	2, 3, 24	cmpt 4226	. 2 class ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) ) )
26	1, 25	wceq 1649	1 wff subringAlg = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) ) )

This definition is referenced by:  sraval  16203