Metamath Proof Explorer

Definition df-sra

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)

Ref Expression
Assertion 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 ) >. ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csra 
 |-  subringAlg
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 6 cpw 
 |-  ~P ( Base ` w )
8 csts 
 |-  sSet
9 csca 
 |-  Scalar
10 cnx 
 |-  ndx
11 10 9 cfv 
 |-  ( Scalar ` ndx )
12 cress 
 |-  |`s
13 3 cv 
 |-  s
14 5 13 12 co 
 |-  ( w |`s s )
15 11 14 cop 
 |-  <. ( Scalar ` ndx ) , ( w |`s s ) >.
16 5 15 8 co 
 |-  ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. )
17 cvsca 
 |-  .s
18 10 17 cfv 
 |-  ( .s ` ndx )
19 cmulr 
 |-  .r
20 5 19 cfv 
 |-  ( .r ` w )
21 18 20 cop 
 |-  <. ( .s ` ndx ) , ( .r ` w ) >.
22 16 21 8 co 
 |-  ( ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. )
23 cip 
 |-  .i
24 10 23 cfv 
 |-  ( .i ` ndx )
25 24 20 cop 
 |-  <. ( .i ` ndx ) , ( .r ` w ) >.
26 22 25 8 co 
 |-  ( ( ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. )
27 3 7 26 cmpt 
 |-  ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. ( Scalar ` ndx ) , ( w |`s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) )
28 1 2 27 cmpt 
 |-  ( 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 ) >. ) ) )
29 0 28 wceq 
 |-  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 ) >. ) ) )