Description: Zero in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pwsmnd.y | |
|
pws0g.z | |
||
Assertion | pws0g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwsmnd.y | |
|
2 | pws0g.z | |
|
3 | eqid | |
|
4 | simpr | |
|
5 | fvexd | |
|
6 | fconst6g | |
|
7 | 6 | adantr | |
8 | 3 4 5 7 | prds0g | |
9 | fconstmpt | |
|
10 | elex | |
|
11 | 10 | ad2antrr | |
12 | fconstmpt | |
|
13 | 12 | a1i | |
14 | fn0g | |
|
15 | 14 | a1i | |
16 | dffn5 | |
|
17 | 15 16 | sylib | |
18 | fveq2 | |
|
19 | 18 2 | eqtr4di | |
20 | 11 13 17 19 | fmptco | |
21 | 9 20 | eqtr4id | |
22 | eqid | |
|
23 | 1 22 | pwsval | |
24 | 23 | fveq2d | |
25 | 8 21 24 | 3eqtr4d | |