Metamath Proof Explorer

Theorem mulclsr

Description: Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulclsr ⊢ 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 mulsrpr ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x y ~ 𝑹 ⋅ 𝑹 z w ~ 𝑹 = x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ~ 𝑹
7 mulclpr ⊢ x ∈ 𝑷 ∧ z ∈ 𝑷 → x ⋅ 𝑷 z ∈ 𝑷
8 mulclpr ⊢ y ∈ 𝑷 ∧ w ∈ 𝑷 → y ⋅ 𝑷 w ∈ 𝑷
9 addclpr ⊢ x ⋅ 𝑷 z ∈ 𝑷 ∧ y ⋅ 𝑷 w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷
10 7 8 9 syl2an ⊢ x ∈ 𝑷 ∧ z ∈ 𝑷 ∧ y ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷
11 10 an4s ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷
12 mulclpr ⊢ x ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 w ∈ 𝑷
13 mulclpr ⊢ y ∈ 𝑷 ∧ z ∈ 𝑷 → y ⋅ 𝑷 z ∈ 𝑷
14 addclpr ⊢ x ⋅ 𝑷 w ∈ 𝑷 ∧ y ⋅ 𝑷 z ∈ 𝑷 → x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
15 12 13 14 syl2an ⊢ x ∈ 𝑷 ∧ w ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
16 15 an42s ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
17 11 16 jca ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷 ∧ x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
18 opelxpi ⊢ x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷 ∧ x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷 × 𝑷
19 enrex ⊢ ~ 𝑹 ∈ V
20 19 ecelqsi ⊢ x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷 × 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
21 17 18 20 3syl ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
22 6 21 eqeltrd ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x y ~ 𝑹 ⋅ 𝑹 z w ~ 𝑹 ∈ 𝑷 × 𝑷 / ~ 𝑹
23 1 3 5 22 2ecoptocl ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A ⋅ 𝑹 B ∈ 𝑷 × 𝑷 / ~ 𝑹
24 23 1 eleqtrrdi ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A ⋅ 𝑹 B ∈ 𝑹