Definition df-sra 13748

Description: Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (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 13746	. 2 class subringAlg
2		vw	. . 3 setvar w
3		cvv 2752	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1363	. . . . . 6 class w
6		cbs 12511	. . . . . 6 class Base
7	5, 6	cfv 5235	. . . . 5 class ( Base ` w )
8	7	cpw 3590	. . . 4 class ~P ( Base ` w )
9		cnx 12508	. . . . . . . . 9 class ndx
10		csca 12589	. . . . . . . . 9 class Scalar
11	9, 10	cfv 5235	. . . . . . . 8 class (Scalar ` ndx )
12	4	cv 1363	. . . . . . . . 9 class s
13		cress 12512	. . . . . . . . 9 class ↾s
14	5, 12, 13	co 5895	. . . . . . . 8 class ( w ↾s s )
15	11, 14	cop 3610	. . . . . . 7 class <. (Scalar ` ndx ) , ( w ↾s s ) >.
16		csts 12509	. . . . . . 7 class sSet
17	5, 15, 16	co 5895	. . . . . 6 class ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. )
18		cvsca 12590	. . . . . . . 8 class .s
19	9, 18	cfv 5235	. . . . . . 7 class ( .s ` ndx )
20		cmulr 12587	. . . . . . . 8 class .r
21	5, 20	cfv 5235	. . . . . . 7 class ( .r ` w )
22	19, 21	cop 3610	. . . . . 6 class <. ( .s ` ndx ) , ( .r ` w ) >.
23	17, 22, 16	co 5895	. . . . 5 class ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. )
24		cip 12591	. . . . . . 7 class .i
25	9, 24	cfv 5235	. . . . . 6 class ( .i ` ndx )
26	25, 21	cop 3610	. . . . 5 class <. ( .i ` ndx ) , ( .r ` w ) >.
27	23, 26, 16	co 5895	. . . 4 class ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. )
28	4, 8, 27	cmpt 4079	. . 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 4079	. 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 1364	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  13750