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

Metamath Proof Explorer

Theorem addcomsr

Description: Addition of signed reals is commutative. (Contributed by NM, 31-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion addcomsr ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 )

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 addsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R )
3 addsrpr ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) = [ ⟨ ( 𝑧 +P 𝑥 ) , ( 𝑤 +P 𝑦 ) ⟩ ] ~R )
4 addcompr ⊢ ( 𝑥 +P 𝑧 ) = ( 𝑧 +P 𝑥 )
5 addcompr ⊢ ( 𝑦 +P 𝑤 ) = ( 𝑤 +P 𝑦 )
6 1 2 3 4 5 ecovcom ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 ) )
7 dmaddsr ⊢ dom +R = ( R × R )
8 7 ndmovcom ⊢ ( ¬ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 ) )
9 6 8 pm2.61i ⊢ ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 )