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	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		oveq1	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 0_{𝑹} = A \cdot_{𝑹} 0_{𝑹}$
3	2	eqeq1d	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to ([⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 0_{𝑹} = 0_{𝑹} \leftrightarrow A \cdot_{𝑹} 0_{𝑹} = 0_{𝑹})$
4		1pr	$⊢ 1_{𝑷} \in 𝑷$
5		mulsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹}$
6	4 4 5	mpanr12	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹}$
7		mulclpr	$⊢ (x \in 𝑷 \land 1_{𝑷} \in 𝑷) \to x \cdot_{𝑷} 1_{𝑷} \in 𝑷$
8	4 7	mpan2	$⊢ x \in 𝑷 \to x \cdot_{𝑷} 1_{𝑷} \in 𝑷$
9		mulclpr	$⊢ (y \in 𝑷 \land 1_{𝑷} \in 𝑷) \to y \cdot_{𝑷} 1_{𝑷} \in 𝑷$
10	4 9	mpan2	$⊢ y \in 𝑷 \to y \cdot_{𝑷} 1_{𝑷} \in 𝑷$
11		addclpr	$⊢ (x \cdot_{𝑷} 1_{𝑷} \in 𝑷 \land y \cdot_{𝑷} 1_{𝑷} \in 𝑷) \to (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
12	8 10 11	syl2an	$⊢ (x \in 𝑷 \land y \in 𝑷) \to (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
13	12 12	anim12i	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷)) \to ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷 \land (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷)$
14		eqid	$⊢ ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷} = ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷}$
15		enreceq	$⊢ (((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷 \land (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷) \land (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to ([⟨(x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷} = ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷})$
16	14 15	mpbiri	$⊢ (((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷 \land (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷) \land (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to [⟨(x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
17	13 16	sylan	$⊢ (((x \in 𝑷 \land y \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷)) \land (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to [⟨(x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
18	4 4 17	mpanr12	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷)) \to [⟨(x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
19	18	anidms	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨(x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
20	6 19	eqtrd	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
21		df-0r	$⊢ 0_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
22	21	oveq2i	$⊢ [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 0_{𝑹} = [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
23	20 22 21	3eqtr4g	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 0_{𝑹} = 0_{𝑹}$
24	1 3 23	ecoptocl	$⊢ A \in 𝑹 \to A \cdot_{𝑹} 0_{𝑹} = 0_{𝑹}$

Metamath Proof Explorer

Theorem 00sr

Proof