Metamath Proof Explorer

Theorem idlsrgstr

Description: A constructed semiring of ideals is a structure. (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypothesis idlsrgstr.1 
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. } )
Assertion idlsrgstr 
|- W Struct <. 1 , ; 1 0 >.

Proof

Step Hyp Ref Expression
1 idlsrgstr.1 
 |-  W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` 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 9nn 
 |-  9 e. NN
5 tsetndx 
 |-  ( TopSet ` ndx ) = 9
6 9lt10 
 |-  9 < ; 1 0
7 10nn 
 |-  ; 1 0 e. NN
8 plendx 
 |-  ( le ` ndx ) = ; 1 0
9 4 5 6 7 8 strle2 
 |-  { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. } Struct <. 9 , ; 1 0 >.
10 3lt9 
 |-  3 < 9
11 3 9 10 strleun 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. } ) Struct <. 1 , ; 1 0 >.
12 1 11 eqbrtri 
 |-  W Struct <. 1 , ; 1 0 >.