Description: 1 is an identity element for multiplication. (Contributed by NM, 2-May-1996) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 1idsr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nr | |
|
2 | oveq1 | |
|
3 | id | |
|
4 | 2 3 | eqeq12d | |
5 | df-1r | |
|
6 | 5 | oveq2i | |
7 | 1pr | |
|
8 | addclpr | |
|
9 | 7 7 8 | mp2an | |
10 | mulsrpr | |
|
11 | 9 7 10 | mpanr12 | |
12 | distrpr | |
|
13 | 1idpr | |
|
14 | 13 | oveq1d | |
15 | 12 14 | eqtr2id | |
16 | distrpr | |
|
17 | 1idpr | |
|
18 | 17 | oveq1d | |
19 | 16 18 | eqtrid | |
20 | 15 19 | oveqan12d | |
21 | addasspr | |
|
22 | ovex | |
|
23 | vex | |
|
24 | ovex | |
|
25 | addcompr | |
|
26 | addasspr | |
|
27 | 22 23 24 25 26 | caov12 | |
28 | 20 21 27 | 3eqtr3g | |
29 | mulclpr | |
|
30 | 9 29 | mpan2 | |
31 | mulclpr | |
|
32 | 7 31 | mpan2 | |
33 | addclpr | |
|
34 | 30 32 33 | syl2an | |
35 | mulclpr | |
|
36 | 7 35 | mpan2 | |
37 | mulclpr | |
|
38 | 9 37 | mpan2 | |
39 | addclpr | |
|
40 | 36 38 39 | syl2an | |
41 | 34 40 | anim12i | |
42 | enreceq | |
|
43 | 41 42 | syldan | |
44 | 43 | anidms | |
45 | 28 44 | mpbird | |
46 | 11 45 | eqtr4d | |
47 | 6 46 | eqtrid | |
48 | 1 4 47 | ecoptocl | |