ipsstr

		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	ipsstr	$⊢ A Struct ⟨1, 8⟩$

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		eqid	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\}$
3	2	rngstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} Struct ⟨1, 3⟩$
4		5nn	$⊢ 5 \in ℕ$
5		scandx	$⊢ Scalar (ndx) = 5$
6		5lt6	$⊢ 5 < 6$
7		6nn	$⊢ 6 \in ℕ$
8		vscandx	$⊢ \cdot_{ndx} = 6$
9		6lt8	$⊢ 6 < 8$
10		8nn	$⊢ 8 \in ℕ$
11		ipndx	$⊢ \cdot_{𝑖} (ndx) = 8$
12	4 5 6 7 8 9 10 11	strle3	$⊢ \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\} Struct ⟨5, 8⟩$
13		3lt5	$⊢ 3 < 5$
14	3 12 13	strleun	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) Struct ⟨1, 8⟩$
15	1 14	eqbrtri	$⊢ A Struct ⟨1, 8⟩$

Metamath Proof Explorer