A ring is an algebra over a subring if and only if that subring is included in its center

[benjub]

It would be nice to prove the equivalence that A is an algebra if and only if the subring is included in the center.

If you really need to get rid of all commutativity or inclusion in the center assumptions, you need the more relaxed notion of R-algebra as an (R, R)-bimodule. (This should be a different definition from df-assa.)

Originally posted by @benjub in #4688 (comment)

[benjub]

Any takers ? @icecream17 ?

[icecream17]

I'm currently busy with refactoring selvvval out of evlsbagval to use in a possible evlsselv, but here's an abstract proof if anyone wants to try.

hypothesis (df-subrg)
    Let S e. SubRing(R)
hypothesis (df-sra)
    Let A = subringAlg(R)(S)
    (i.e. R = Base(A)
          S = Scalar(A)
          scalar multiplication = vector/ring multiplication)
hypothesis (df-cntr)
    Let Z = Cntr(R)

Then S C_ Z iff A e. AssAlg

Proof:
If S C_ Z, then A e. AssAlg
   (sx)y = s(xy) by assoc
   sxy = xsy because sx = xs by ( ~ cntri )
                                because s e. S and S C_ Z -> s e. Z

If A e. AssAlg, then S C_ Z
   We have sxy = xsy by ( ~ assaassr ), set y to 1 -> sx = xs
      (-> s e. Z by [new library ~ elcntr from ~ cntrval, and ~ elcntz or ~ cntzel])
   (or make new library ~ sscntr )

(The proof skips converting between scalar and vector/ring multiplication since they're the same by hypothesis df-sra)