Theorem 1idsr

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

	Ref	Expression
Assertion	1idsr	⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 1R ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-nr	⊢ R = ( ( P × P ) / ~R )
2		oveq1	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 1R ) = ( 𝐴 ·R 1R ) )
3		id	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 )
4	2 3	eqeq12d	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 1R ) = [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ ( 𝐴 ·R 1R ) = 𝐴 ) )
5		df-1r	⊢ 1R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R
6	5	oveq2i	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 1R ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R )
7		1pr	⊢ 1P ∈ P
8		addclpr	⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
9	7 7 8	mp2an	⊢ ( 1P +P 1P ) ∈ P
10		mulsrpr	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ⟩ ] ~R )
11	9 7 10	mpanr12	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ⟩ ] ~R )
12		distrpr	⊢ ( 𝑥 ·P ( 1P +P 1P ) ) = ( ( 𝑥 ·P 1P ) +P ( 𝑥 ·P 1P ) )
13		1idpr	⊢ ( 𝑥 ∈ P → ( 𝑥 ·P 1P ) = 𝑥 )
14	13	oveq1d	⊢ ( 𝑥 ∈ P → ( ( 𝑥 ·P 1P ) +P ( 𝑥 ·P 1P ) ) = ( 𝑥 +P ( 𝑥 ·P 1P ) ) )
15	12 14	syl5req	⊢ ( 𝑥 ∈ P → ( 𝑥 +P ( 𝑥 ·P 1P ) ) = ( 𝑥 ·P ( 1P +P 1P ) ) )
16		distrpr	⊢ ( 𝑦 ·P ( 1P +P 1P ) ) = ( ( 𝑦 ·P 1P ) +P ( 𝑦 ·P 1P ) )
17		1idpr	⊢ ( 𝑦 ∈ P → ( 𝑦 ·P 1P ) = 𝑦 )
18	17	oveq1d	⊢ ( 𝑦 ∈ P → ( ( 𝑦 ·P 1P ) +P ( 𝑦 ·P 1P ) ) = ( 𝑦 +P ( 𝑦 ·P 1P ) ) )
19	16 18	syl5eq	⊢ ( 𝑦 ∈ P → ( 𝑦 ·P ( 1P +P 1P ) ) = ( 𝑦 +P ( 𝑦 ·P 1P ) ) )
20	15 19	oveqan12d	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑥 +P ( 𝑥 ·P 1P ) ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) = ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 +P ( 𝑦 ·P 1P ) ) ) )
21		addasspr	⊢ ( ( 𝑥 +P ( 𝑥 ·P 1P ) ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) = ( 𝑥 +P ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) )
22		ovex	⊢ ( 𝑥 ·P ( 1P +P 1P ) ) ∈ V
23		vex	⊢ 𝑦 ∈ V
24		ovex	⊢ ( 𝑦 ·P 1P ) ∈ V
25		addcompr	⊢ ( 𝑧 +P 𝑤 ) = ( 𝑤 +P 𝑧 )
26		addasspr	⊢ ( ( 𝑧 +P 𝑤 ) +P 𝑣 ) = ( 𝑧 +P ( 𝑤 +P 𝑣 ) )
27	22 23 24 25 26	caov12	⊢ ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 +P ( 𝑦 ·P 1P ) ) ) = ( 𝑦 +P ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) )
28	20 21 27	3eqtr3g	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑥 +P ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ) = ( 𝑦 +P ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ) )
29		mulclpr	⊢ ( ( 𝑥 ∈ P ∧ ( 1P +P 1P ) ∈ P ) → ( 𝑥 ·P ( 1P +P 1P ) ) ∈ P )
30	9 29	mpan2	⊢ ( 𝑥 ∈ P → ( 𝑥 ·P ( 1P +P 1P ) ) ∈ P )
31		mulclpr	⊢ ( ( 𝑦 ∈ P ∧ 1P ∈ P ) → ( 𝑦 ·P 1P ) ∈ P )
32	7 31	mpan2	⊢ ( 𝑦 ∈ P → ( 𝑦 ·P 1P ) ∈ P )
33		addclpr	⊢ ( ( ( 𝑥 ·P ( 1P +P 1P ) ) ∈ P ∧ ( 𝑦 ·P 1P ) ∈ P ) → ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ∈ P )
34	30 32 33	syl2an	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ∈ P )
35		mulclpr	⊢ ( ( 𝑥 ∈ P ∧ 1P ∈ P ) → ( 𝑥 ·P 1P ) ∈ P )
36	7 35	mpan2	⊢ ( 𝑥 ∈ P → ( 𝑥 ·P 1P ) ∈ P )
37		mulclpr	⊢ ( ( 𝑦 ∈ P ∧ ( 1P +P 1P ) ∈ P ) → ( 𝑦 ·P ( 1P +P 1P ) ) ∈ P )
38	9 37	mpan2	⊢ ( 𝑦 ∈ P → ( 𝑦 ·P ( 1P +P 1P ) ) ∈ P )
39		addclpr	⊢ ( ( ( 𝑥 ·P 1P ) ∈ P ∧ ( 𝑦 ·P ( 1P +P 1P ) ) ∈ P ) → ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ∈ P )
40	36 38 39	syl2an	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ∈ P )
41	34 40	anim12i	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → ( ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ∈ P ∧ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ∈ P ) )
42		enreceq	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ∈ P ∧ ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ⟩ ] ~R ↔ ( 𝑥 +P ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ) = ( 𝑦 +P ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ) ) )
43	41 42	syldan	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ⟩ ] ~R ↔ ( 𝑥 +P ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ) = ( 𝑦 +P ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ) ) )
44	43	anidms	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ⟩ ] ~R ↔ ( 𝑥 +P ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ) = ( 𝑦 +P ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) ) ) )
45	28 44	mpbird	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = [ ⟨ ( ( 𝑥 ·P ( 1P +P 1P ) ) +P ( 𝑦 ·P 1P ) ) , ( ( 𝑥 ·P 1P ) +P ( 𝑦 ·P ( 1P +P 1P ) ) ) ⟩ ] ~R )
46	11 45	eqtr4d	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R )
47	6 46	syl5eq	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 1R ) = [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R )
48	1 4 47	ecoptocl	⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 1R ) = 𝐴 )