This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}$
	Assertion	ipsmulr	$⊢ \underset{˙}{\times} \in V \to \underset{˙}{\times} = \cdot_{A}$

Proof

Step	Hyp	Ref	Expression
1		ipspart.a	$⊢ A = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}$
2	1	ipsstr	$⊢ A Struct ⟨1, 8⟩$
3		mulridx	$⊢ \cdot_{𝑟} = Slot \cdot_{ndx}$
4		snsstp3	$⊢ \{⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\}$
5		ssun1	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}$
6	5 1	sseqtrri	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \subseteq A$
7	4 6	sstri	$⊢ \{⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \subseteq A$
8	2 3 7	strfv	$⊢ \underset{˙}{\times} \in V \to \underset{˙}{\times} = \cdot_{A}$