Metamath Proof Explorer

Theorem 0idsr

Description: The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion 0idsr ( 𝐴 ∈ R → ( 𝐴 +R 0R ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 oveq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R 0R ) = ( 𝐴 +R 0R ) )
3 id ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 )
4 2 3 eqeq12d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R 0R ) = [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ ( 𝐴 +R 0R ) = 𝐴 ) )
5 df-0r ⊢ 0R = [ ⟨ 1P , 1P ⟩ ] ~R
6 5 oveq2i ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R 0R ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 1P , 1P ⟩ ] ~R )
7 1pr ⊢ 1P ∈ P
8 addsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 1P ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 1P , 1P ⟩ ] ~R ) = [ ⟨ ( 𝑥 +P 1P ) , ( 𝑦 +P 1P ) ⟩ ] ~R )
9 7 7 8 mpanr12 ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 1P , 1P ⟩ ] ~R ) = [ ⟨ ( 𝑥 +P 1P ) , ( 𝑦 +P 1P ) ⟩ ] ~R )
10 addclpr ⊢ ( ( 𝑥 ∈ P ∧ 1P ∈ P ) → ( 𝑥 +P 1P ) ∈ P )
11 7 10 mpan2 ⊢ ( 𝑥 ∈ P → ( 𝑥 +P 1P ) ∈ P )
12 addclpr ⊢ ( ( 𝑦 ∈ P ∧ 1P ∈ P ) → ( 𝑦 +P 1P ) ∈ P )
13 7 12 mpan2 ⊢ ( 𝑦 ∈ P → ( 𝑦 +P 1P ) ∈ P )
14 11 13 anim12i ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑥 +P 1P ) ∈ P ∧ ( 𝑦 +P 1P ) ∈ P ) )
15 vex ⊢ 𝑥 ∈ V
16 vex ⊢ 𝑦 ∈ V
17 7 elexi ⊢ 1P ∈ V
18 addcompr ⊢ ( 𝑧 +P 𝑤 ) = ( 𝑤 +P 𝑧 )
19 addasspr ⊢ ( ( 𝑧 +P 𝑤 ) +P 𝑣 ) = ( 𝑧 +P ( 𝑤 +P 𝑣 ) )
20 15 16 17 18 19 caov12 ⊢ ( 𝑥 +P ( 𝑦 +P 1P ) ) = ( 𝑦 +P ( 𝑥 +P 1P ) )
21 enreceq ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( ( 𝑥 +P 1P ) ∈ P ∧ ( 𝑦 +P 1P ) ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ ( 𝑥 +P 1P ) , ( 𝑦 +P 1P ) ⟩ ] ~R ↔ ( 𝑥 +P ( 𝑦 +P 1P ) ) = ( 𝑦 +P ( 𝑥 +P 1P ) ) ) )
22 20 21 mpbiri ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( ( 𝑥 +P 1P ) ∈ P ∧ ( 𝑦 +P 1P ) ∈ P ) ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ ( 𝑥 +P 1P ) , ( 𝑦 +P 1P ) ⟩ ] ~R )
23 14 22 mpdan ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ ( 𝑥 +P 1P ) , ( 𝑦 +P 1P ) ⟩ ] ~R )
24 9 23 eqtr4d ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 1P , 1P ⟩ ] ~R ) = [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R )
25 6 24 syl5eq ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R 0R ) = [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R )
26 1 4 25 ecoptocl ⊢ ( 𝐴 ∈ R → ( 𝐴 +R 0R ) = 𝐴 )