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 )