Metamath Proof Explorer


Theorem algsca

Description: The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypothesis algpart.a A=BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙
Assertion algsca SVS=ScalarA

Proof

Step Hyp Ref Expression
1 algpart.a A=BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙
2 1 algstr AStruct16
3 scaid Scalar=SlotScalarndx
4 snsspr1 ScalarndxSScalarndxSndx·˙
5 ssun2 ScalarndxSndx·˙BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙
6 5 1 sseqtrri ScalarndxSndx·˙A
7 4 6 sstri ScalarndxSA
8 2 3 7 strfv SVS=ScalarA