Metamath Proof Explorer


Theorem odrngplusg

Description: The addition operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypothesis odrngstr.w W=BasendxB+ndx+˙ndx·˙TopSetndxJndx˙distndxD
Assertion odrngplusg +˙V+˙=+W

Proof

Step Hyp Ref Expression
1 odrngstr.w W=BasendxB+ndx+˙ndx·˙TopSetndxJndx˙distndxD
2 1 odrngstr WStruct112
3 plusgid +𝑔=Slot+ndx
4 snsstp2 +ndx+˙BasendxB+ndx+˙ndx·˙
5 ssun1 BasendxB+ndx+˙ndx·˙BasendxB+ndx+˙ndx·˙TopSetndxJndx˙distndxD
6 5 1 sseqtrri BasendxB+ndx+˙ndx·˙W
7 4 6 sstri +ndx+˙W
8 2 3 7 strfv +˙V+˙=+W