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 ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A + 𝑹 B ∈ 𝑹

Proof

Step Hyp Ref Expression
1 df-nr ⊢ 𝑹 = 𝑷 × 𝑷 / ~ 𝑹
2 oveq1 ⊢ x y ~ 𝑹 = A → x y ~ 𝑹 + 𝑹 z w ~ 𝑹 = A + 𝑹 z w ~ 𝑹
3 2 eleq1d ⊢ x y ~ 𝑹 = A → x y ~ 𝑹 + 𝑹 z w ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹 ↔ A + 𝑹 z w ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
4 oveq2 ⊢ z w ~ 𝑹 = B → A + 𝑹 z w ~ 𝑹 = A + 𝑹 B
5 4 eleq1d ⊢ z w ~ 𝑹 = B → A + 𝑹 z w ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹 ↔ A + 𝑹 B ∈ 𝑷 × 𝑷 / ~ 𝑹
6 addsrpr ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x y ~ 𝑹 + 𝑹 z w ~ 𝑹 = x + 𝑷 z y + 𝑷 w ~ 𝑹
7 addclpr ⊢ x ∈ 𝑷 ∧ z ∈ 𝑷 → x + 𝑷 z ∈ 𝑷
8 addclpr ⊢ y ∈ 𝑷 ∧ w ∈ 𝑷 → y + 𝑷 w ∈ 𝑷
9 7 8 anim12i ⊢ x ∈ 𝑷 ∧ z ∈ 𝑷 ∧ y ∈ 𝑷 ∧ w ∈ 𝑷 → x + 𝑷 z ∈ 𝑷 ∧ y + 𝑷 w ∈ 𝑷
10 9 an4s ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x + 𝑷 z ∈ 𝑷 ∧ y + 𝑷 w ∈ 𝑷
11 opelxpi ⊢ x + 𝑷 z ∈ 𝑷 ∧ y + 𝑷 w ∈ 𝑷 → x + 𝑷 z y + 𝑷 w ∈ 𝑷 × 𝑷
12 enrex ⊢ ~ 𝑹 ∈ V
13 12 ecelqsi ⊢ x + 𝑷 z y + 𝑷 w ∈ 𝑷 × 𝑷 → x + 𝑷 z y + 𝑷 w ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
14 10 11 13 3syl ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x + 𝑷 z y + 𝑷 w ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
15 6 14 eqeltrd ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x y ~ 𝑹 + 𝑹 z w ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
16 1 3 5 15 2ecoptocl ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A + 𝑹 B ∈ 𝑷 × 𝑷 / ~ 𝑹
17 16 1 eleqtrrdi ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A + 𝑹 B ∈ 𝑹