Definition df-sra 17686

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

Distinct variable group:   w, s

Detailed syntax breakdown of Definition df-sra

Step	Hyp	Ref	Expression
1		csra 17682	. 2 class subringAlg
2		vw	. . 3 setvar w
3		cvv 3093	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1380	. . . . . 6 class w
6		cbs 14504	. . . . . 6 class Base
7	5, 6	cfv 5574	. . . . 5 class ( Base ` w )
8	7	cpw 3993	. . . 4 class ~P ( Base ` w )
9		cnx 14501	. . . . . . . . 9 class ndx
10		csca 14572	. . . . . . . . 9 class Scalar
11	9, 10	cfv 5574	. . . . . . . 8 class (Scalar ` ndx )
12	4	cv 1380	. . . . . . . . 9 class s
13		cress 14505	. . . . . . . . 9 class ↾s
14	5, 12, 13	co 6277	. . . . . . . 8 class ( w ↾s s )
15	11, 14	cop 4016	. . . . . . 7 class <. (Scalar ` ndx ) , ( w ↾s s ) >.
16		csts 14502	. . . . . . 7 class sSet
17	5, 15, 16	co 6277	. . . . . 6 class ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. )
18		cvsca 14573	. . . . . . . 8 class .s
19	9, 18	cfv 5574	. . . . . . 7 class ( .s ` ndx )
20		cmulr 14570	. . . . . . . 8 class .r
21	5, 20	cfv 5574	. . . . . . 7 class ( .r ` w )
22	19, 21	cop 4016	. . . . . 6 class <. ( .s ` ndx ) , ( .r ` w ) >.
23	17, 22, 16	co 6277	. . . . 5 class ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. )
24		cip 14574	. . . . . . 7 class .i
25	9, 24	cfv 5574	. . . . . 6 class ( .i ` ndx )
26	25, 21	cop 4016	. . . . 5 class <. ( .i ` ndx ) , ( .r ` w ) >.
27	23, 26, 16	co 6277	. . . 4 class ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. )
28	4, 8, 27	cmpt 4491	. . 3 class ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) )
29	2, 3, 28	cmpt 4491	. 2 class ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) )
30	1, 29	wceq 1381	1 wff subringAlg = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) )

This definition is referenced by:  sraval  17690