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	|- R = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. }
Assertion	rngstr	|- R Struct <. 1 , 3 >.

Proof

Step	Hyp	Ref	Expression
1		rngfn.r	|- R = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. }
2		1nn	|- 1 e. NN
3		basendx	|- ( Base ` ndx ) = 1
4		1lt2	|- 1 < 2
5		2nn	|- 2 e. NN
6		plusgndx	|- ( +g ` ndx ) = 2
7		2lt3	|- 2 < 3
8		3nn	|- 3 e. NN
9		mulrndx	|- ( .r ` ndx ) = 3
10	2 3 4 5 6 7 8 9	strle3	|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } Struct <. 1 , 3 >.
11	1 10	eqbrtri	|- R Struct <. 1 , 3 >.