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

Metamath Proof Explorer

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 ⟩