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

Metamath Proof Explorer

Theorem srngstr

Description: A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypothesis srngstr.r ⊢ 𝑅 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
Assertion srngstr 𝑅 Struct ⟨ 1 , 4 ⟩

Proof

Step Hyp Ref Expression
1 srngstr.r ⊢ 𝑅 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ 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 4nn ⊢ 4 ∈ ℕ
5 starvndx ⊢ ( *𝑟 ‘ ndx ) = 4
6 4 5 strle1 ⊢ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } Struct ⟨ 4 , 4 ⟩
7 3lt4 ⊢ 3 < 4
8 3 6 7 strleun ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) Struct ⟨ 1 , 4 ⟩
9 1 8 eqbrtri ⊢ 𝑅 Struct ⟨ 1 , 4 ⟩