Description: Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pwsplusgval.y | |
|
pwsplusgval.b | |
||
pwsplusgval.r | |
||
pwsplusgval.i | |
||
pwsplusgval.f | |
||
pwsplusgval.g | |
||
pwsplusgval.a | |
||
pwsplusgval.p | |
||
Assertion | pwsplusgval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwsplusgval.y | |
|
2 | pwsplusgval.b | |
|
3 | pwsplusgval.r | |
|
4 | pwsplusgval.i | |
|
5 | pwsplusgval.f | |
|
6 | pwsplusgval.g | |
|
7 | pwsplusgval.a | |
|
8 | pwsplusgval.p | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | fvexd | |
|
12 | fnconstg | |
|
13 | 3 12 | syl | |
14 | eqid | |
|
15 | 1 14 | pwsval | |
16 | 3 4 15 | syl2anc | |
17 | 16 | fveq2d | |
18 | 2 17 | eqtrid | |
19 | 5 18 | eleqtrd | |
20 | 6 18 | eleqtrd | |
21 | eqid | |
|
22 | 9 10 11 4 13 19 20 21 | prdsplusgval | |
23 | fvconst2g | |
|
24 | 3 23 | sylan | |
25 | 24 | fveq2d | |
26 | 25 7 | eqtr4di | |
27 | 26 | oveqd | |
28 | 27 | mpteq2dva | |
29 | 22 28 | eqtrd | |
30 | 16 | fveq2d | |
31 | 8 30 | eqtrid | |
32 | 31 | oveqd | |
33 | fvexd | |
|
34 | fvexd | |
|
35 | eqid | |
|
36 | 1 35 2 3 4 5 | pwselbas | |
37 | 36 | feqmptd | |
38 | 1 35 2 3 4 6 | pwselbas | |
39 | 38 | feqmptd | |
40 | 4 33 34 37 39 | offval2 | |
41 | 29 32 40 | 3eqtr4d | |