Description: The key property of projections: the sum of all the projections of A is A . (Contributed by Mario Carneiro, 26-Apr-2016) (Revised by AV, 14-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dpjfval.1 | |
|
dpjfval.2 | |
||
dpjfval.p | |
||
dpjidcl.3 | |
||
dpjidcl.0 | |
||
dpjidcl.w | |
||
Assertion | dpjidcl | |