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

Metamath Proof Explorer

Theorem ipsip

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	ipsip	$⊢ I \in V \to I = \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		ipid	$⊢ \cdot_{𝑖} = Slot \cdot_{𝑖} (ndx)$
4		snsstp3	$⊢ \{⟨\cdot_{𝑖} (ndx), I⟩\} \subseteq \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}$
5		ssun2	$⊢ \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\} \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	$⊢ \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\} \subseteq A$
7	4 6	sstri	$⊢ \{⟨\cdot_{𝑖} (ndx), I⟩\} \subseteq A$
8	2 3 7	strfv	$⊢ I \in V \to I = \cdot_{𝑖} (A)$