This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
Assertion odrngstr 𝑊 Struct ⟨ 1 , 1 2 ⟩

Proof

Step Hyp Ref Expression
1 odrngstr.w ⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
2 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ }
3 2 rngstr ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } Struct ⟨ 1 , 3 ⟩
4 9nn ⊢ 9 ∈ ℕ
5 tsetndx ⊢ ( TopSet ‘ ndx ) = 9
6 9lt10 ⊢ 9 < 1 0
7 10nn ⊢ 1 0 ∈ ℕ
8 plendx ⊢ ( le ‘ ndx ) = 1 0
9 1nn0 ⊢ 1 ∈ ℕ0
10 0nn0 ⊢ 0 ∈ ℕ0
11 2nn ⊢ 2 ∈ ℕ
12 2pos ⊢ 0 < 2
13 9 10 11 12 declt ⊢ 1 0 < 1 2
14 9 11 decnncl ⊢ 1 2 ∈ ℕ
15 dsndx ⊢ ( dist ‘ ndx ) = 1 2
16 4 5 6 7 8 13 14 15 strle3 ⊢ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } Struct ⟨ 9 , 1 2 ⟩
17 3lt9 ⊢ 3 < 9
18 3 16 17 strleun ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ) Struct ⟨ 1 , 1 2 ⟩
19 1 18 eqbrtri ⊢ 𝑊 Struct ⟨ 1 , 1 2 ⟩