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

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 
|- .- = ( -g ` ZZring )
Assertion zringsub 
|- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X .- Y ) = ( X - Y ) )

Proof

Step Hyp Ref Expression
1 zringsub.p 
 |-  .- = ( -g ` ZZring )
2 zcn 
 |-  ( x e. ZZ -> x e. CC )
3 zaddcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
4 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
5 0z 
 |-  0 e. ZZ
6 2 3 4 5 cnsubglem 
 |-  ZZ e. ( SubGrp ` CCfld )
7 cnfldsub 
 |-  - = ( -g ` CCfld )
8 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
9 7 8 1 subgsub 
 |-  ( ( ZZ e. ( SubGrp ` CCfld ) /\ X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )
10 6 9 mp3an1 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )
11 10 eqcomd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( X .- Y ) = ( X - Y ) )