Metamath Proof Explorer


Theorem zringsub

Description: The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025)

Ref Expression
Hypothesis zringsub.p - ˙ = - ring
Assertion zringsub X Y X - ˙ Y = X Y

Proof

Step Hyp Ref Expression
1 zringsub.p - ˙ = - ring
2 zcn x x
3 zaddcl x y x + y
4 znegcl x x
5 0z 0
6 2 3 4 5 cnsubglem SubGrp fld
7 cnfldsub = - fld
8 df-zring ring = fld 𝑠
9 7 8 1 subgsub SubGrp fld X Y X Y = X - ˙ Y
10 6 9 mp3an1 X Y X Y = X - ˙ Y
11 10 eqcomd X Y X - ˙ Y = X Y