Metamath Proof Explorer

Theorem addasssr

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

Ref Expression
Assertion addasssr ( ( 𝐴 +R 𝐵 ) +R 𝐶 ) = ( 𝐴 +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 addsrpr ⊢ ( ( ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R +R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 +P 𝑧 ) +P 𝑣 ) , ( ( 𝑦 +P 𝑤 ) +P 𝑢 ) ⟩ ] ~R )
5 addsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( ( 𝑧 +P 𝑣 ) ∈ P ∧ ( 𝑤 +P 𝑢 ) ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ ( 𝑧 +P 𝑣 ) , ( 𝑤 +P 𝑢 ) ⟩ ] ~R ) = [ ⟨ ( 𝑥 +P ( 𝑧 +P 𝑣 ) ) , ( 𝑦 +P ( 𝑤 +P 𝑢 ) ) ⟩ ] ~R )
6 addclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 +P 𝑧 ) ∈ P )
7 addclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑦 +P 𝑤 ) ∈ P )
8 6 7 anim12i ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) )
9 8 an4s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) )
10 addclpr ⊢ ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑧 +P 𝑣 ) ∈ P )
11 addclpr ⊢ ( ( 𝑤 ∈ P ∧ 𝑢 ∈ P ) → ( 𝑤 +P 𝑢 ) ∈ P )
12 10 11 anim12i ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑤 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑧 +P 𝑣 ) ∈ P ∧ ( 𝑤 +P 𝑢 ) ∈ P ) )
13 12 an4s ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑧 +P 𝑣 ) ∈ P ∧ ( 𝑤 +P 𝑢 ) ∈ P ) )
14 addasspr ⊢ ( ( 𝑥 +P 𝑧 ) +P 𝑣 ) = ( 𝑥 +P ( 𝑧 +P 𝑣 ) )
15 addasspr ⊢ ( ( 𝑦 +P 𝑤 ) +P 𝑢 ) = ( 𝑦 +P ( 𝑤 +P 𝑢 ) )
16 1 2 3 4 5 9 13 14 15 ecovass ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R ) → ( ( 𝐴 +R 𝐵 ) +R 𝐶 ) = ( 𝐴 +R ( 𝐵 +R 𝐶 ) ) )
17 dmaddsr ⊢ dom +R = ( R × R )
18 0nsr ⊢ ¬ ∅ ∈ R
19 17 18 ndmovass ⊢ ( ¬ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R ) → ( ( 𝐴 +R 𝐵 ) +R 𝐶 ) = ( 𝐴 +R ( 𝐵 +R 𝐶 ) ) )
20 16 19 pm2.61i ⊢ ( ( 𝐴 +R 𝐵 ) +R 𝐶 ) = ( 𝐴 +R ( 𝐵 +R 𝐶 ) )