Description: Projective subspace sum operation. (Contributed by NM, 29-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | paddfval.l | |
|
paddfval.j | |
||
paddfval.a | |
||
paddfval.p | |
||
Assertion | paddfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | paddfval.l | |
|
2 | paddfval.j | |
|
3 | paddfval.a | |
|
4 | paddfval.p | |
|
5 | elex | |
|
6 | fveq2 | |
|
7 | 6 3 | eqtr4di | |
8 | 7 | pweqd | |
9 | eqidd | |
|
10 | fveq2 | |
|
11 | 10 1 | eqtr4di | |
12 | fveq2 | |
|
13 | 12 2 | eqtr4di | |
14 | 13 | oveqd | |
15 | 9 11 14 | breq123d | |
16 | 15 | 2rexbidv | |
17 | 7 16 | rabeqbidv | |
18 | 17 | uneq2d | |
19 | 8 8 18 | mpoeq123dv | |
20 | df-padd | |
|
21 | 3 | fvexi | |
22 | 21 | pwex | |
23 | 22 22 | mpoex | |
24 | 19 20 23 | fvmpt | |
25 | 4 24 | eqtrid | |
26 | 5 25 | syl | |