Metamath Proof Explorer


Theorem ipsmulr

Description: The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 29-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypothesis ipspart.a A=BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndxI
Assertion ipsmulr ×˙V×˙=A

Proof

Step Hyp Ref Expression
1 ipspart.a A=BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndxI
2 1 ipsstr AStruct18
3 mulrid 𝑟=Slotndx
4 snsstp3 ndx×˙BasendxB+ndx+˙ndx×˙
5 ssun1 BasendxB+ndx+˙ndx×˙BasendxB+ndx+˙ndx×˙ScalarndxSndx·˙𝑖ndxI
6 5 1 sseqtrri BasendxB+ndx+˙ndx×˙A
7 4 6 sstri ndx×˙A
8 2 3 7 strfv ×˙V×˙=A