Metamath Proof Explorer

Theorem re1m1e0m0

Description: Equality of two left-additive identities. See resubidaddid1 . Uses ax-i2m1 . (Contributed by SN, 25-Dec-2023)

Ref Expression
Assertion re1m1e0m0 
|- ( 1 -R 1 ) = ( 0 -R 0 )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( T. -> 0 e. RR )
2 1re 
 |-  1 e. RR
3 rersubcl 
 |-  ( ( 1 e. RR /\ 1 e. RR ) -> ( 1 -R 1 ) e. RR )
4 2 2 3 mp2an 
 |-  ( 1 -R 1 ) e. RR
5 4 a1i 
 |-  ( T. -> ( 1 -R 1 ) e. RR )
6 ax-icn 
 |-  _i e. CC
7 6 6 mulcli 
 |-  ( _i x. _i ) e. CC
8 ax-1cn 
 |-  1 e. CC
9 4 recni 
 |-  ( 1 -R 1 ) e. CC
10 7 8 9 addassi 
 |-  ( ( ( _i x. _i ) + 1 ) + ( 1 -R 1 ) ) = ( ( _i x. _i ) + ( 1 + ( 1 -R 1 ) ) )
11 repncan3 
 |-  ( ( 1 e. RR /\ 1 e. RR ) -> ( 1 + ( 1 -R 1 ) ) = 1 )
12 2 2 11 mp2an 
 |-  ( 1 + ( 1 -R 1 ) ) = 1
13 12 oveq2i 
 |-  ( ( _i x. _i ) + ( 1 + ( 1 -R 1 ) ) ) = ( ( _i x. _i ) + 1 )
14 10 13 eqtri 
 |-  ( ( ( _i x. _i ) + 1 ) + ( 1 -R 1 ) ) = ( ( _i x. _i ) + 1 )
15 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
16 15 oveq1i 
 |-  ( ( ( _i x. _i ) + 1 ) + ( 1 -R 1 ) ) = ( 0 + ( 1 -R 1 ) )
17 14 16 15 3eqtr3i 
 |-  ( 0 + ( 1 -R 1 ) ) = 0
18 17 a1i 
 |-  ( T. -> ( 0 + ( 1 -R 1 ) ) = 0 )
19 1 5 18 reladdrsub 
 |-  ( T. -> ( 1 -R 1 ) = ( 0 -R 0 ) )
20 19 mptru 
 |-  ( 1 -R 1 ) = ( 0 -R 0 )