# Metamath Proof Explorer

## Theorem 00sr

Description: A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion 00sr ${⊢}{A}\in 𝑹\to {A}{\cdot }_{𝑹}{0}_{𝑹}={0}_{𝑹}$

### Proof

Step Hyp Ref Expression
1 df-nr ${⊢}𝑹=\left(𝑷×𝑷\right)/{~}_{𝑹}$
2 oveq1 ${⊢}\left[⟨{x},{y}⟩\right]{~}_{𝑹}={A}\to \left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}={A}{\cdot }_{𝑹}{0}_{𝑹}$
3 2 eqeq1d ${⊢}\left[⟨{x},{y}⟩\right]{~}_{𝑹}={A}\to \left(\left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}={0}_{𝑹}↔{A}{\cdot }_{𝑹}{0}_{𝑹}={0}_{𝑹}\right)$
4 1pr ${⊢}{1}_{𝑷}\in 𝑷$
5 mulsrpr ${⊢}\left(\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\wedge \left({1}_{𝑷}\in 𝑷\wedge {1}_{𝑷}\in 𝑷\right)\right)\to \left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}=\left[⟨\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right),\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)⟩\right]{~}_{𝑹}$
6 4 4 5 mpanr12 ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}=\left[⟨\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right),\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)⟩\right]{~}_{𝑹}$
7 mulclpr ${⊢}\left({x}\in 𝑷\wedge {1}_{𝑷}\in 𝑷\right)\to {x}{\cdot }_{𝑷}{1}_{𝑷}\in 𝑷$
8 4 7 mpan2 ${⊢}{x}\in 𝑷\to {x}{\cdot }_{𝑷}{1}_{𝑷}\in 𝑷$
9 mulclpr ${⊢}\left({y}\in 𝑷\wedge {1}_{𝑷}\in 𝑷\right)\to {y}{\cdot }_{𝑷}{1}_{𝑷}\in 𝑷$
10 4 9 mpan2 ${⊢}{y}\in 𝑷\to {y}{\cdot }_{𝑷}{1}_{𝑷}\in 𝑷$
11 addclpr ${⊢}\left({x}{\cdot }_{𝑷}{1}_{𝑷}\in 𝑷\wedge {y}{\cdot }_{𝑷}{1}_{𝑷}\in 𝑷\right)\to \left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷$
12 8 10 11 syl2an ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷$
13 12 12 anim12i ${⊢}\left(\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\wedge \left({x}\in 𝑷\wedge {y}\in 𝑷\right)\right)\to \left(\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷\wedge \left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷\right)$
14 eqid ${⊢}\left(\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\right){+}_{𝑷}{1}_{𝑷}=\left(\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\right){+}_{𝑷}{1}_{𝑷}$
15 enreceq ${⊢}\left(\left(\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷\wedge \left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷\right)\wedge \left({1}_{𝑷}\in 𝑷\wedge {1}_{𝑷}\in 𝑷\right)\right)\to \left(\left[⟨\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right),\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)⟩\right]{~}_{𝑹}=\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}↔\left(\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\right){+}_{𝑷}{1}_{𝑷}=\left(\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\right){+}_{𝑷}{1}_{𝑷}\right)$
16 14 15 mpbiri ${⊢}\left(\left(\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷\wedge \left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)\in 𝑷\right)\wedge \left({1}_{𝑷}\in 𝑷\wedge {1}_{𝑷}\in 𝑷\right)\right)\to \left[⟨\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right),\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)⟩\right]{~}_{𝑹}=\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}$
17 13 16 sylan ${⊢}\left(\left(\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\wedge \left({x}\in 𝑷\wedge {y}\in 𝑷\right)\right)\wedge \left({1}_{𝑷}\in 𝑷\wedge {1}_{𝑷}\in 𝑷\right)\right)\to \left[⟨\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right),\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)⟩\right]{~}_{𝑹}=\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}$
18 4 4 17 mpanr12 ${⊢}\left(\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\wedge \left({x}\in 𝑷\wedge {y}\in 𝑷\right)\right)\to \left[⟨\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right),\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)⟩\right]{~}_{𝑹}=\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}$
19 18 anidms ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left[⟨\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right),\left({x}{\cdot }_{𝑷}{1}_{𝑷}\right){+}_{𝑷}\left({y}{\cdot }_{𝑷}{1}_{𝑷}\right)⟩\right]{~}_{𝑹}=\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}$
20 6 19 eqtrd ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}=\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}$
21 df-0r ${⊢}{0}_{𝑹}=\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}$
22 21 oveq2i ${⊢}\left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=\left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}\left[⟨{1}_{𝑷},{1}_{𝑷}⟩\right]{~}_{𝑹}$
23 20 22 21 3eqtr4g ${⊢}\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\to \left[⟨{x},{y}⟩\right]{~}_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}={0}_{𝑹}$
24 1 3 23 ecoptocl ${⊢}{A}\in 𝑹\to {A}{\cdot }_{𝑹}{0}_{𝑹}={0}_{𝑹}$