Metamath Proof Explorer


Theorem rngstr

Description: A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013) (Revised by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypothesis rngfn.r 𝑅 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ }
Assertion rngstr 𝑅 Struct ⟨ 1 , 3 ⟩

Proof

Step Hyp Ref Expression
1 rngfn.r 𝑅 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ }
2 1nn 1 ∈ ℕ
3 basendx ( Base ‘ ndx ) = 1
4 1lt2 1 < 2
5 2nn 2 ∈ ℕ
6 plusgndx ( +g ‘ ndx ) = 2
7 2lt3 2 < 3
8 3nn 3 ∈ ℕ
9 mulrndx ( .r ‘ ndx ) = 3
10 2 3 4 5 6 7 8 9 strle3 { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } Struct ⟨ 1 , 3 ⟩
11 1 10 eqbrtri 𝑅 Struct ⟨ 1 , 3 ⟩