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 ⊢xy~𝑹=A→xy~𝑹⋅𝑹zw~𝑹=A⋅𝑹zw~𝑹
3 2 eleq1d ⊢xy~𝑹=A→xy~𝑹⋅𝑹zw~𝑹∈𝑷×𝑷/~𝑹↔A⋅𝑹zw~𝑹∈𝑷×𝑷/~𝑹
4 oveq2 ⊢zw~𝑹=B→A⋅𝑹zw~𝑹=A⋅𝑹B
5 4 eleq1d ⊢zw~𝑹=B→A⋅𝑹zw~𝑹∈𝑷×𝑷/~𝑹↔A⋅𝑹B∈𝑷×𝑷/~𝑹
6 mulsrpr ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→xy~𝑹⋅𝑹zw~𝑹=x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷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⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z∈𝑷×𝑷
19 enrex ⊢~𝑹∈V
20 19 ecelqsi ⊢x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z∈𝑷×𝑷→x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z~𝑹∈𝑷×𝑷/~𝑹
21 17 18 20 3syl ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→x⋅𝑷z+𝑷y⋅𝑷wx⋅𝑷w+𝑷y⋅𝑷z~𝑹∈𝑷×𝑷/~𝑹
22 6 21 eqeltrd ⊢x∈𝑷∧y∈𝑷∧z∈𝑷∧w∈𝑷→xy~𝑹⋅𝑹zw~𝑹∈𝑷×𝑷/~𝑹
23 1 3 5 22 2ecoptocl ⊢A∈𝑹∧B∈𝑹→A⋅𝑹B∈𝑷×𝑷/~𝑹
24 23 1 eleqtrrdi ⊢A∈𝑹∧B∈𝑹→A⋅𝑹B∈𝑹