Theorem ipval2lem3

Description: Lemma for ipval3 . (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dipfval.1	|- X = ( BaseSet ` U )
	dipfval.2	|- G = ( +v ` U )
	dipfval.4	|- S = ( .sOLD ` U )
	dipfval.6	|- N = ( normCV ` U )
	dipfval.7	|- P = ( .iOLD ` U )
Assertion	ipval2lem3	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G B ) ) ^ 2 ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		dipfval.1	|- X = ( BaseSet ` U )
2		dipfval.2	|- G = ( +v ` U )
3		dipfval.4	|- S = ( .sOLD ` U )
4		dipfval.6	|- N = ( normCV ` U )
5		dipfval.7	|- P = ( .iOLD ` U )
6	1 3	nvsid	|- ( ( U e. NrmCVec /\ B e. X ) -> ( 1 S B ) = B )
7	6	oveq2d	|- ( ( U e. NrmCVec /\ B e. X ) -> ( A G ( 1 S B ) ) = ( A G B ) )
8	7	fveq2d	|- ( ( U e. NrmCVec /\ B e. X ) -> ( N ` ( A G ( 1 S B ) ) ) = ( N ` ( A G B ) ) )
9	8	oveq1d	|- ( ( U e. NrmCVec /\ B e. X ) -> ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) = ( ( N ` ( A G B ) ) ^ 2 ) )
10	9	3adant2	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) = ( ( N ` ( A G B ) ) ^ 2 ) )
11		ax-1cn	|- 1 e. CC
12	1 2 3 4 5	ipval2lem2	|- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ 1 e. CC ) -> ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) e. RR )
13	11 12	mpan2	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) e. RR )
14	10 13	eqeltrrd	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G B ) ) ^ 2 ) e. RR )