This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtr2id ⊢ ( 𝑥 ∈ 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 eqtrid ⊢ ( 𝑦 ∈ 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 eqtrid ⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R 1R ) = [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R )
48 1 4 47 ecoptocl ⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 1R ) = 𝐴 )