Metamath Proof Explorer

Theorem sn-00idlem3

Description: Lemma for sn-00id . (Contributed by SN, 25-Dec-2023)

Ref Expression
Assertion sn-00idlem3 
|- ( ( 0 -R 0 ) = 1 -> ( 0 + 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( ( 0 -R 0 ) = 1 -> ( 0 x. ( 0 -R 0 ) ) = ( 0 x. 1 ) )
2 0re 
 |-  0 e. RR
3 sn-00idlem1 
 |-  ( 0 e. RR -> ( 0 x. ( 0 -R 0 ) ) = ( 0 -R 0 ) )
4 2 3 ax-mp 
 |-  ( 0 x. ( 0 -R 0 ) ) = ( 0 -R 0 )
5 ax-1rid 
 |-  ( 0 e. RR -> ( 0 x. 1 ) = 0 )
6 2 5 ax-mp 
 |-  ( 0 x. 1 ) = 0
7 1 4 6 3eqtr3g 
 |-  ( ( 0 -R 0 ) = 1 -> ( 0 -R 0 ) = 0 )
8 7 oveq1d 
 |-  ( ( 0 -R 0 ) = 1 -> ( ( 0 -R 0 ) + 0 ) = ( 0 + 0 ) )
9 resubidaddlid 
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> ( ( 0 -R 0 ) + 0 ) = 0 )
10 2 2 9 mp2an 
 |-  ( ( 0 -R 0 ) + 0 ) = 0
11 8 10 eqtr3di 
 |-  ( ( 0 -R 0 ) = 1 -> ( 0 + 0 ) = 0 )