0idsr

Description: The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	0idsr	$⊢ A \in 𝑹 \to A +_{𝑹} 0_{𝑹} = A$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		oveq1	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} 0_{𝑹} = A +_{𝑹} 0_{𝑹}$
3		id	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to [⟨x, y⟩] ~_{𝑹} = A$
4	2 3	eqeq12d	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to ([⟨x, y⟩] ~_{𝑹} +_{𝑹} 0_{𝑹} = [⟨x, y⟩] ~_{𝑹} \leftrightarrow A +_{𝑹} 0_{𝑹} = A)$
5		df-0r	$⊢ 0_{𝑹} = [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
6	5	oveq2i	$⊢ [⟨x, y⟩] ~_{𝑹} +_{𝑹} 0_{𝑹} = [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
7		1pr	$⊢ 1_{𝑷} \in 𝑷$
8		addsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨x +_{𝑷} 1_{𝑷}, y +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
9	7 7 8	mpanr12	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨x +_{𝑷} 1_{𝑷}, y +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
10		addclpr	$⊢ (x \in 𝑷 \land 1_{𝑷} \in 𝑷) \to x +_{𝑷} 1_{𝑷} \in 𝑷$
11	7 10	mpan2	$⊢ x \in 𝑷 \to x +_{𝑷} 1_{𝑷} \in 𝑷$
12		addclpr	$⊢ (y \in 𝑷 \land 1_{𝑷} \in 𝑷) \to y +_{𝑷} 1_{𝑷} \in 𝑷$
13	7 12	mpan2	$⊢ y \in 𝑷 \to y +_{𝑷} 1_{𝑷} \in 𝑷$
14	11 13	anim12i	$⊢ (x \in 𝑷 \land y \in 𝑷) \to (x +_{𝑷} 1_{𝑷} \in 𝑷 \land y +_{𝑷} 1_{𝑷} \in 𝑷)$
15		vex	$⊢ x \in V$
16		vex	$⊢ y \in V$
17	7	elexi	$⊢ 1_{𝑷} \in V$
18		addcompr	$⊢ z +_{𝑷} w = w +_{𝑷} z$
19		addasspr	$⊢ (z +_{𝑷} w) +_{𝑷} v = z +_{𝑷} (w +_{𝑷} v)$
20	15 16 17 18 19	caov12	$⊢ x +_{𝑷} (y +_{𝑷} 1_{𝑷}) = y +_{𝑷} (x +_{𝑷} 1_{𝑷})$
21		enreceq	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (x +_{𝑷} 1_{𝑷} \in 𝑷 \land y +_{𝑷} 1_{𝑷} \in 𝑷)) \to ([⟨x, y⟩] ~_{𝑹} = [⟨x +_{𝑷} 1_{𝑷}, y +_{𝑷} 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow x +_{𝑷} (y +_{𝑷} 1_{𝑷}) = y +_{𝑷} (x +_{𝑷} 1_{𝑷}))$
22	20 21	mpbiri	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (x +_{𝑷} 1_{𝑷} \in 𝑷 \land y +_{𝑷} 1_{𝑷} \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} = [⟨x +_{𝑷} 1_{𝑷}, y +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
23	14 22	mpdan	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} = [⟨x +_{𝑷} 1_{𝑷}, y +_{𝑷} 1_{𝑷}⟩] ~_{𝑹}$
24	9 23	eqtr4d	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨x, y⟩] ~_{𝑹}$
25	6 24	syl5eq	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} 0_{𝑹} = [⟨x, y⟩] ~_{𝑹}$
26	1 4 25	ecoptocl	$⊢ A \in 𝑹 \to A +_{𝑹} 0_{𝑹} = A$

Metamath Proof Explorer

Theorem 0idsr

Proof