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

Metamath Proof Explorer

Theorem resubgval

Description: Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypothesis resubgval.m 
|- .- = ( -g ` RRfld )
Assertion resubgval 
|- ( ( X e. RR /\ Y e. RR ) -> ( X - Y ) = ( X .- Y ) )

Proof

Step Hyp Ref Expression
1 resubgval.m 
 |-  .- = ( -g ` RRfld )
2 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
3 2 simpli 
 |-  RR e. ( SubRing ` CCfld )
4 subrgsubg 
 |-  ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) )
5 3 4 ax-mp 
 |-  RR e. ( SubGrp ` CCfld )
6 cnfldsub 
 |-  - = ( -g ` CCfld )
7 df-refld 
 |-  RRfld = ( CCfld |`s RR )
8 6 7 1 subgsub 
 |-  ( ( RR e. ( SubGrp ` CCfld ) /\ X e. RR /\ Y e. RR ) -> ( X - Y ) = ( X .- Y ) )
9 5 8 mp3an1 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( X - Y ) = ( X .- Y ) )