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

Metamath Proof Explorer

Theorem addclsr

Description: Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995) (New usage is discouraged.)

Ref Expression
Assertion addclsr ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) ∈ R )

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 oveq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) )
3 2 eleq1d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ↔ ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ) )
4 oveq2 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 +R 𝐵 ) )
5 4 eleq1d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( ( 𝐴 +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ↔ ( 𝐴 +R 𝐵 ) ∈ ( ( P × P ) / ~R ) ) )
6 addsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R )
7 addclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 +P 𝑧 ) ∈ P )
8 addclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑦 +P 𝑤 ) ∈ P )
9 7 8 anim12i ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) )
10 9 an4s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) )
11 opelxpi ⊢ ( ( ( 𝑥 +P 𝑧 ) ∈ P ∧ ( 𝑦 +P 𝑤 ) ∈ P ) → ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ∈ ( P × P ) )
12 enrex ⊢ ~R ∈ V
13 12 ecelqsi ⊢ ( ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ∈ ( P × P ) → [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
14 10 11 13 3syl ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
15 6 14 eqeltrd ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) )
16 1 3 5 15 2ecoptocl ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) ∈ ( ( P × P ) / ~R ) )
17 16 1 eleqtrrdi ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) ∈ R )