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