Description: Value of the ring unit in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pws1.y | |
|
pws1.o | |
||
Assertion | pws1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pws1.y | |
|
2 | pws1.o | |
|
3 | eqid | |
|
4 | 1 3 | pwsval | |
5 | 4 | fveq2d | |
6 | eqid | |
|
7 | simpr | |
|
8 | fvexd | |
|
9 | fconst6g | |
|
10 | 9 | adantr | |
11 | 6 7 8 10 | prds1 | |
12 | fn0g | |
|
13 | fnmgp | |
|
14 | ssv | |
|
15 | 14 | a1i | |
16 | fnco | |
|
17 | 12 13 15 16 | mp3an12i | |
18 | df-ur | |
|
19 | 18 | fneq1i | |
20 | 17 19 | sylibr | |
21 | elex | |
|
22 | 21 | adantr | |
23 | fcoconst | |
|
24 | 20 22 23 | syl2anc | |
25 | 2 | sneqi | |
26 | 25 | xpeq2i | |
27 | 24 26 | eqtr4di | |
28 | 5 11 27 | 3eqtr2rd | |