Description: Equation 6.47 of Ponnusamy p. 362. (Contributed by NM, 27-Apr-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ip1i.1 | |- X = ( BaseSet ` U ) |
|
ip1i.2 | |- G = ( +v ` U ) |
||
ip1i.4 | |- S = ( .sOLD ` U ) |
||
ip1i.7 | |- P = ( .iOLD ` U ) |
||
ip1i.9 | |- U e. CPreHilOLD |
||
ip1i.a | |- A e. X |
||
ip1i.b | |- B e. X |
||
ip1i.c | |- C e. X |
||
Assertion | ip1i | |- ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) = ( 2 x. ( A P C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ip1i.1 | |- X = ( BaseSet ` U ) |
|
2 | ip1i.2 | |- G = ( +v ` U ) |
|
3 | ip1i.4 | |- S = ( .sOLD ` U ) |
|
4 | ip1i.7 | |- P = ( .iOLD ` U ) |
|
5 | ip1i.9 | |- U e. CPreHilOLD |
|
6 | ip1i.a | |- A e. X |
|
7 | ip1i.b | |- B e. X |
|
8 | ip1i.c | |- C e. X |
|
9 | eqid | |- ( normCV ` U ) = ( normCV ` U ) |
|
10 | ax-1cn | |- 1 e. CC |
|
11 | 1 2 3 4 5 6 7 8 9 10 | ip1ilem | |- ( ( ( A G B ) P C ) + ( ( A G ( -u 1 S B ) ) P C ) ) = ( 2 x. ( A P C ) ) |