Description: Value of the ring unit in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prds1.y | |
|
prds1.i | |
||
prds1.s | |
||
prds1.r | |
||
Assertion | prds1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prds1.y | |
|
2 | prds1.i | |
|
3 | prds1.s | |
|
4 | prds1.r | |
|
5 | eqid | |
|
6 | mgpf | |
|
7 | fco2 | |
|
8 | 6 4 7 | sylancr | |
9 | 5 2 3 8 | prds0g | |
10 | eqidd | |
|
11 | eqid | |
|
12 | 4 | ffnd | |
13 | 1 11 5 2 3 12 | prdsmgp | |
14 | 13 | simpld | |
15 | 13 | simprd | |
16 | 15 | oveqdr | |
17 | 10 14 16 | grpidpropd | |
18 | 9 17 | eqtr4d | |
19 | df-ur | |
|
20 | 19 | coeq1i | |
21 | coass | |
|
22 | 20 21 | eqtri | |
23 | eqid | |
|
24 | 11 23 | ringidval | |
25 | 18 22 24 | 3eqtr4g | |