Merge developments of R^n

[metamath]

Merge developments of R^n

[sorear]

Side note: df-plig has a broken link, should be http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf

[digama0]

@sorear Fixed in 04f3414.

[tirix]

I think it's worth mentioning in this issue this definition proposed in a post by Mario and another post by Mario
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ' ( ( ringLMod ' ( CCfld |'s RR ) ) freeLMod i ) ) ) $.
df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ' i ) |'s { f e. ( RR ^m i ) | ( '' f ( _V \ { 0 } ) ) e. Fin } ) ) $.
df-prds $a |- Xs_ = ... u. { <. ( .i ' ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ' x ) ( .i ' ( r ' x ) ) ( g ' x ) ) ) ) ) >. }

[tirix]

The first step, to update ~ df-prds, is done in #931.

The next step, which is not listed above, would be to also update ~ df-sra subringAlg to define its inner product as the ring multiplication. Am I correct?

[tirix]

Second step, with the definition of RR^ and EEhil (to follow the naming convention for structures), is done in #937.

A third step would be to pull-in Jeff Madsen's metric.