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

Proof

Step Hyp Ref Expression
1 srngstr.r 
 |-  R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )
2 eqid 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. }
3 2 rngstr 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } Struct <. 1 , 3 >.
4 4nn 
 |-  4 e. NN
5 starvndx 
 |-  ( *r ` ndx ) = 4
6 4 5 strle1 
 |-  { <. ( *r ` ndx ) , .* >. } Struct <. 4 , 4 >.
7 3lt4 
 |-  3 < 4
8 3 6 7 strleun 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } ) Struct <. 1 , 4 >.
9 1 8 eqbrtri 
 |-  R Struct <. 1 , 4 >.