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 ⟩