Metamath Proof Explorer


Theorem ipsbase

Description: The base set 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 = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx I
Assertion ipsbase B V B = Base A

Proof

Step Hyp Ref Expression
1 ipspart.a A = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx I
2 1 ipsstr A Struct 1 8
3 baseid Base = Slot Base ndx
4 snsstp1 Base ndx B Base ndx B + ndx + ˙ ndx × ˙
5 ssun1 Base ndx B + ndx + ˙ ndx × ˙ Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx I
6 5 1 sseqtrri Base ndx B + ndx + ˙ ndx × ˙ A
7 4 6 sstri Base ndx B A
8 2 3 7 strfv B V B = Base A