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

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 ( 𝐴 ∈ R → ( 𝐴 ·R 0R ) = 0R )

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 oveq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 0R ) = ( 𝐴 ·R 0R ) )
3 2 eqeq1d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 0R ) = 0R ↔ ( 𝐴 ·R 0R ) = 0R ) )
4 1pr ⊢ 1P ∈ P
5 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 1P ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 1P , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ⟩ ] ~R )
6 4 4 5 mpanr12 ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 1P , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ⟩ ] ~R )
7 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 1P ∈ P ) → ( 𝑥 ·P 1P ) ∈ P )
8 4 7 mpan2 ⊢ ( 𝑥 ∈ P → ( 𝑥 ·P 1P ) ∈ P )
9 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 1P ∈ P ) → ( 𝑦 ·P 1P ) ∈ P )
10 4 9 mpan2 ⊢ ( 𝑦 ∈ P → ( 𝑦 ·P 1P ) ∈ P )
11 addclpr ⊢ ( ( ( 𝑥 ·P 1P ) ∈ P ∧ ( 𝑦 ·P 1P ) ∈ P ) → ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P )
12 8 10 11 syl2an ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P )
13 12 12 anim12i ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → ( ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P ∧ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P ) )
14 eqid ⊢ ( ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) +P 1P ) = ( ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) +P 1P )
15 enreceq ⊢ ( ( ( ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P ∧ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P ) ∧ ( 1P ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ⟩ ] ~R = [ ⟨ 1P , 1P ⟩ ] ~R ↔ ( ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) +P 1P ) = ( ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) +P 1P ) ) )
16 14 15 mpbiri ⊢ ( ( ( ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P ∧ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ∈ P ) ∧ ( 1P ∈ P ∧ 1P ∈ P ) ) → [ ⟨ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ⟩ ] ~R = [ ⟨ 1P , 1P ⟩ ] ~R )
17 13 16 sylan ⊢ ( ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) ∧ ( 1P ∈ P ∧ 1P ∈ P ) ) → [ ⟨ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ⟩ ] ~R = [ ⟨ 1P , 1P ⟩ ] ~R )
18 4 4 17 mpanr12 ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → [ ⟨ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ⟩ ] ~R = [ ⟨ 1P , 1P ⟩ ] ~R )
19 18 anidms ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → [ ⟨ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P 1P ) ) ⟩ ] ~R = [ ⟨ 1P , 1P ⟩ ] ~R )
20 6 19 eqtrd ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 1P , 1P ⟩ ] ~R ) = [ ⟨ 1P , 1P ⟩ ] ~R )
21 df-0r ⊢ 0R = [ ⟨ 1P , 1P ⟩ ] ~R
22 21 oveq2i ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 0R ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 1P , 1P ⟩ ] ~R )
23 20 22 21 3eqtr4g ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 0R ) = 0R )
24 1 3 23 ecoptocl ⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 0R ) = 0R )