Theorem ipsstr

Description: Lemma to shorten proofs of ipsbase through ipsvsca . (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	⊢ 𝐴 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝐼 ⟩ } )
Assertion	ipsstr	⊢ 𝐴 Struct ⟨ 1 , 8 ⟩

Proof

Step	Hyp	Ref	Expression
1		ipspart.a	⊢ 𝐴 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝐼 ⟩ } )
2		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ }
3	2	rngstr	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } Struct ⟨ 1 , 3 ⟩
4		5nn	⊢ 5 ∈ ℕ
5		scandx	⊢ ( Scalar ‘ ndx ) = 5
6		5lt6	⊢ 5 < 6
7		6nn	⊢ 6 ∈ ℕ
8		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
9		6lt8	⊢ 6 < 8
10		8nn	⊢ 8 ∈ ℕ
11		ipndx	⊢ ( ·𝑖 ‘ ndx ) = 8
12	4 5 6 7 8 9 10 11	strle3	⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝐼 ⟩ } Struct ⟨ 5 , 8 ⟩
13		3lt5	⊢ 3 < 5
14	3 12 13	strleun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝐼 ⟩ } ) Struct ⟨ 1 , 8 ⟩
15	1 14	eqbrtri	⊢ 𝐴 Struct ⟨ 1 , 8 ⟩