Metamath Proof Explorer


Theorem odrngstr

Description: Functionality of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015) (Proof shortened by AV, 15-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 odrngstr.w
 |-  W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )
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 1nn0
 |-  1 e. NN0
10 0nn0
 |-  0 e. NN0
11 2nn
 |-  2 e. NN
12 2pos
 |-  0 < 2
13 9 10 11 12 declt
 |-  ; 1 0 < ; 1 2
14 9 11 decnncl
 |-  ; 1 2 e. NN
15 dsndx
 |-  ( dist ` ndx ) = ; 1 2
16 4 5 6 7 8 13 14 15 strle3
 |-  { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } Struct <. 9 , ; 1 2 >.
17 3lt9
 |-  3 < 9
18 3 16 17 strleun
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) Struct <. 1 , ; 1 2 >.
19 1 18 eqbrtri
 |-  W Struct <. 1 , ; 1 2 >.