Metamath Proof Explorer

Theorem bj-rvecssabl

Description: (The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019)

Ref Expression
Assertion bj-rvecssabl 
|- RRVec C_ Abel

Proof

Step Hyp Ref Expression
1 bj-rvecssmod 
 |-  RRVec C_ LMod
2 bj-modssabl 
 |-  LMod C_ Abel
3 1 2 sstri 
 |-  RRVec C_ Abel