1idsr

Description: 1 is an identity element for multiplication. (Contributed by NM, 2-May-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	1idsr	$⊢ A \in 𝑹 \to A \cdot_{𝑹} 1_{𝑹} = A$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		oveq1	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 1_{𝑹} = A \cdot_{𝑹} 1_{𝑹}$
3		id	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to [⟨x, y⟩] ~_{𝑹} = A$
4	2 3	eqeq12d	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to ([⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 1_{𝑹} = [⟨x, y⟩] ~_{𝑹} \leftrightarrow A \cdot_{𝑹} 1_{𝑹} = A)$
5		df-1r	$⊢ 1_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
6	5	oveq2i	$⊢ [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 1_{𝑹} = [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
7		1pr	$⊢ 1_{𝑷} \in 𝑷$
8		addclpr	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
9	7 7 8	mp2an	$⊢ 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
10		mulsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹}$
11	9 7 10	mpanr12	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹}$
12		distrpr	$⊢ x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) = (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (x \cdot_{𝑷} 1_{𝑷})$
13		1idpr	$⊢ x \in 𝑷 \to x \cdot_{𝑷} 1_{𝑷} = x$
14	13	oveq1d	$⊢ x \in 𝑷 \to (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (x \cdot_{𝑷} 1_{𝑷}) = x +_{𝑷} (x \cdot_{𝑷} 1_{𝑷})$
15	12 14	syl5req	$⊢ x \in 𝑷 \to x +_{𝑷} (x \cdot_{𝑷} 1_{𝑷}) = x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})$
16		distrpr	$⊢ y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) = (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})$
17		1idpr	$⊢ y \in 𝑷 \to y \cdot_{𝑷} 1_{𝑷} = y$
18	17	oveq1d	$⊢ y \in 𝑷 \to (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) = y +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})$
19	16 18	syl5eq	$⊢ y \in 𝑷 \to y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) = y +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})$
20	15 19	oveqan12d	$⊢ (x \in 𝑷 \land y \in 𝑷) \to (x +_{𝑷} (x \cdot_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) = (x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}))$
21		addasspr	$⊢ (x +_{𝑷} (x \cdot_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) = x +_{𝑷} ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})))$
22		ovex	$⊢ x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in V$
23		vex	$⊢ y \in V$
24		ovex	$⊢ y \cdot_{𝑷} 1_{𝑷} \in V$
25		addcompr	$⊢ z +_{𝑷} w = w +_{𝑷} z$
26		addasspr	$⊢ (z +_{𝑷} w) +_{𝑷} v = z +_{𝑷} (w +_{𝑷} v)$
27	22 23 24 25 26	caov12	$⊢ (x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})) = y +_{𝑷} ((x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}))$
28	20 21 27	3eqtr3g	$⊢ (x \in 𝑷 \land y \in 𝑷) \to x +_{𝑷} ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))) = y +_{𝑷} ((x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}))$
29		mulclpr	$⊢ (x \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷) \to x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
30	9 29	mpan2	$⊢ x \in 𝑷 \to x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
31		mulclpr	$⊢ (y \in 𝑷 \land 1_{𝑷} \in 𝑷) \to y \cdot_{𝑷} 1_{𝑷} \in 𝑷$
32	7 31	mpan2	$⊢ y \in 𝑷 \to y \cdot_{𝑷} 1_{𝑷} \in 𝑷$
33		addclpr	$⊢ (x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷 \land y \cdot_{𝑷} 1_{𝑷} \in 𝑷) \to (x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
34	30 32 33	syl2an	$⊢ (x \in 𝑷 \land y \in 𝑷) \to (x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
35		mulclpr	$⊢ (x \in 𝑷 \land 1_{𝑷} \in 𝑷) \to x \cdot_{𝑷} 1_{𝑷} \in 𝑷$
36	7 35	mpan2	$⊢ x \in 𝑷 \to x \cdot_{𝑷} 1_{𝑷} \in 𝑷$
37		mulclpr	$⊢ (y \in 𝑷 \land 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷) \to y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
38	9 37	mpan2	$⊢ y \in 𝑷 \to y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷$
39		addclpr	$⊢ (x \cdot_{𝑷} 1_{𝑷} \in 𝑷 \land y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) \in 𝑷) \to (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) \in 𝑷$
40	36 38 39	syl2an	$⊢ (x \in 𝑷 \land y \in 𝑷) \to (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) \in 𝑷$
41	34 40	anim12i	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷)) \to ((x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷 \land (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) \in 𝑷)$
42		enreceq	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land ((x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}) \in 𝑷 \land (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) \in 𝑷)) \to ([⟨x, y⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹} \leftrightarrow x +_{𝑷} ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))) = y +_{𝑷} ((x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})))$
43	41 42	syldan	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷)) \to ([⟨x, y⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹} \leftrightarrow x +_{𝑷} ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))) = y +_{𝑷} ((x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})))$
44	43	anidms	$⊢ (x \in 𝑷 \land y \in 𝑷) \to ([⟨x, y⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹} \leftrightarrow x +_{𝑷} ((x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))) = y +_{𝑷} ((x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})))$
45	28 44	mpbird	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷}), (x \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (y \cdot_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹}$
46	11 45	eqtr4d	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨x, y⟩] ~_{𝑹}$
47	6 46	syl5eq	$⊢ (x \in 𝑷 \land y \in 𝑷) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} 1_{𝑹} = [⟨x, y⟩] ~_{𝑹}$
48	1 4 47	ecoptocl	$⊢ A \in 𝑹 \to A \cdot_{𝑹} 1_{𝑹} = A$

Metamath Proof Explorer

Theorem 1idsr

Proof