Metamath Proof Explorer


Theorem ip1i

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 ) )

Proof

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 ) )