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 1 oveq1d
 |-  ( ( 0 -R 0 ) = 1 -> ( ( 0 x. ( 0 -R 0 ) ) + 0 ) = ( ( 0 x. 1 ) + 0 ) )
3 0re
 |-  0 e. RR
4 sn-00idlem1
 |-  ( 0 e. RR -> ( 0 x. ( 0 -R 0 ) ) = ( 0 -R 0 ) )
5 4 adantr
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> ( 0 x. ( 0 -R 0 ) ) = ( 0 -R 0 ) )
6 5 oveq1d
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> ( ( 0 x. ( 0 -R 0 ) ) + 0 ) = ( ( 0 -R 0 ) + 0 ) )
7 resubidaddid1
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> ( ( 0 -R 0 ) + 0 ) = 0 )
8 6 7 eqtrd
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> ( ( 0 x. ( 0 -R 0 ) ) + 0 ) = 0 )
9 3 3 8 mp2an
 |-  ( ( 0 x. ( 0 -R 0 ) ) + 0 ) = 0
10 9 a1i
 |-  ( ( 0 -R 0 ) = 1 -> ( ( 0 x. ( 0 -R 0 ) ) + 0 ) = 0 )
11 ax-1rid
 |-  ( 0 e. RR -> ( 0 x. 1 ) = 0 )
12 3 11 mp1i
 |-  ( ( 0 -R 0 ) = 1 -> ( 0 x. 1 ) = 0 )
13 12 oveq1d
 |-  ( ( 0 -R 0 ) = 1 -> ( ( 0 x. 1 ) + 0 ) = ( 0 + 0 ) )
14 2 10 13 3eqtr3rd
 |-  ( ( 0 -R 0 ) = 1 -> ( 0 + 0 ) = 0 )