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 A𝑹A𝑹1𝑹=A

Proof

Step Hyp Ref Expression
1 df-nr 𝑹=𝑷×𝑷/~𝑹
2 oveq1 xy~𝑹=Axy~𝑹𝑹1𝑹=A𝑹1𝑹
3 id xy~𝑹=Axy~𝑹=A
4 2 3 eqeq12d xy~𝑹=Axy~𝑹𝑹1𝑹=xy~𝑹A𝑹1𝑹=A
5 df-1r 1𝑹=1𝑷+𝑷1𝑷1𝑷~𝑹
6 5 oveq2i xy~𝑹𝑹1𝑹=xy~𝑹𝑹1𝑷+𝑷1𝑷1𝑷~𝑹
7 1pr 1𝑷𝑷
8 addclpr 1𝑷𝑷1𝑷𝑷1𝑷+𝑷1𝑷𝑷
9 7 7 8 mp2an 1𝑷+𝑷1𝑷𝑷
10 mulsrpr x𝑷y𝑷1𝑷+𝑷1𝑷𝑷1𝑷𝑷xy~𝑹𝑹1𝑷+𝑷1𝑷1𝑷~𝑹=x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷~𝑹
11 9 7 10 mpanr12 x𝑷y𝑷xy~𝑹𝑹1𝑷+𝑷1𝑷1𝑷~𝑹=x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷~𝑹
12 distrpr x𝑷1𝑷+𝑷1𝑷=x𝑷1𝑷+𝑷x𝑷1𝑷
13 1idpr x𝑷x𝑷1𝑷=x
14 13 oveq1d x𝑷x𝑷1𝑷+𝑷x𝑷1𝑷=x+𝑷x𝑷1𝑷
15 12 14 eqtr2id x𝑷x+𝑷x𝑷1𝑷=x𝑷1𝑷+𝑷1𝑷
16 distrpr y𝑷1𝑷+𝑷1𝑷=y𝑷1𝑷+𝑷y𝑷1𝑷
17 1idpr y𝑷y𝑷1𝑷=y
18 17 oveq1d y𝑷y𝑷1𝑷+𝑷y𝑷1𝑷=y+𝑷y𝑷1𝑷
19 16 18 eqtrid y𝑷y𝑷1𝑷+𝑷1𝑷=y+𝑷y𝑷1𝑷
20 15 19 oveqan12d x𝑷y𝑷x+𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷=x𝑷1𝑷+𝑷1𝑷+𝑷y+𝑷y𝑷1𝑷
21 addasspr x+𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷=x+𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷
22 ovex x𝑷1𝑷+𝑷1𝑷V
23 vex yV
24 ovex y𝑷1𝑷V
25 addcompr z+𝑷w=w+𝑷z
26 addasspr z+𝑷w+𝑷v=z+𝑷w+𝑷v
27 22 23 24 25 26 caov12 x𝑷1𝑷+𝑷1𝑷+𝑷y+𝑷y𝑷1𝑷=y+𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷
28 20 21 27 3eqtr3g x𝑷y𝑷x+𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷=y+𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷
29 mulclpr x𝑷1𝑷+𝑷1𝑷𝑷x𝑷1𝑷+𝑷1𝑷𝑷
30 9 29 mpan2 x𝑷x𝑷1𝑷+𝑷1𝑷𝑷
31 mulclpr y𝑷1𝑷𝑷y𝑷1𝑷𝑷
32 7 31 mpan2 y𝑷y𝑷1𝑷𝑷
33 addclpr x𝑷1𝑷+𝑷1𝑷𝑷y𝑷1𝑷𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷𝑷
34 30 32 33 syl2an x𝑷y𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷𝑷
35 mulclpr x𝑷1𝑷𝑷x𝑷1𝑷𝑷
36 7 35 mpan2 x𝑷x𝑷1𝑷𝑷
37 mulclpr y𝑷1𝑷+𝑷1𝑷𝑷y𝑷1𝑷+𝑷1𝑷𝑷
38 9 37 mpan2 y𝑷y𝑷1𝑷+𝑷1𝑷𝑷
39 addclpr x𝑷1𝑷𝑷y𝑷1𝑷+𝑷1𝑷𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷𝑷
40 36 38 39 syl2an x𝑷y𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷𝑷
41 34 40 anim12i x𝑷y𝑷x𝑷y𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷𝑷
42 enreceq x𝑷y𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷𝑷xy~𝑹=x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷~𝑹x+𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷=y+𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷
43 41 42 syldan x𝑷y𝑷x𝑷y𝑷xy~𝑹=x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷~𝑹x+𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷=y+𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷
44 43 anidms x𝑷y𝑷xy~𝑹=x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷~𝑹x+𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷=y+𝑷x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷
45 28 44 mpbird x𝑷y𝑷xy~𝑹=x𝑷1𝑷+𝑷1𝑷+𝑷y𝑷1𝑷x𝑷1𝑷+𝑷y𝑷1𝑷+𝑷1𝑷~𝑹
46 11 45 eqtr4d x𝑷y𝑷xy~𝑹𝑹1𝑷+𝑷1𝑷1𝑷~𝑹=xy~𝑹
47 6 46 eqtrid x𝑷y𝑷xy~𝑹𝑹1𝑹=xy~𝑹
48 1 4 47 ecoptocl A𝑹A𝑹1𝑹=A