Metamath Proof Explorer

Theorem ipasslem9

Description: Lemma for ipassi . Conclude from ipasslem8 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-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
ipasslem9.a 
|- A e. X
ipasslem9.b 
|- B e. X
Assertion ipasslem9 
|- ( C e. RR -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) )

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 ipasslem9.a 
 |-  A e. X
7 ipasslem9.b 
 |-  B e. X
8 oveq1 
 |-  ( w = C -> ( w S A ) = ( C S A ) )
9 8 oveq1d 
 |-  ( w = C -> ( ( w S A ) P B ) = ( ( C S A ) P B ) )
10 oveq1 
 |-  ( w = C -> ( w x. ( A P B ) ) = ( C x. ( A P B ) ) )
11 9 10 oveq12d 
 |-  ( w = C -> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) = ( ( ( C S A ) P B ) - ( C x. ( A P B ) ) ) )
12 eqid 
 |-  ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) = ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) )
13 ovex 
 |-  ( ( ( C S A ) P B ) - ( C x. ( A P B ) ) ) e. _V
14 11 12 13 fvmpt 
 |-  ( C e. RR -> ( ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) ` C ) = ( ( ( C S A ) P B ) - ( C x. ( A P B ) ) ) )
15 1 2 3 4 5 6 7 12 ipasslem8 
 |-  ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) : RR --> { 0 }
16 fvconst 
 |-  ( ( ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) : RR --> { 0 } /\ C e. RR ) -> ( ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) ` C ) = 0 )
17 15 16 mpan 
 |-  ( C e. RR -> ( ( w e. RR |-> ( ( ( w S A ) P B ) - ( w x. ( A P B ) ) ) ) ` C ) = 0 )
18 14 17 eqtr3d 
 |-  ( C e. RR -> ( ( ( C S A ) P B ) - ( C x. ( A P B ) ) ) = 0 )
19 recn 
 |-  ( C e. RR -> C e. CC )
20 5 phnvi 
 |-  U e. NrmCVec
21 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ C e. CC /\ A e. X ) -> ( C S A ) e. X )
22 20 6 21 mp3an13 
 |-  ( C e. CC -> ( C S A ) e. X )
23 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ ( C S A ) e. X /\ B e. X ) -> ( ( C S A ) P B ) e. CC )
24 20 7 23 mp3an13 
 |-  ( ( C S A ) e. X -> ( ( C S A ) P B ) e. CC )
25 22 24 syl 
 |-  ( C e. CC -> ( ( C S A ) P B ) e. CC )
26 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
27 20 6 7 26 mp3an 
 |-  ( A P B ) e. CC
28 mulcl 
 |-  ( ( C e. CC /\ ( A P B ) e. CC ) -> ( C x. ( A P B ) ) e. CC )
29 27 28 mpan2 
 |-  ( C e. CC -> ( C x. ( A P B ) ) e. CC )
30 25 29 subeq0ad 
 |-  ( C e. CC -> ( ( ( ( C S A ) P B ) - ( C x. ( A P B ) ) ) = 0 <-> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) )
31 19 30 syl 
 |-  ( C e. RR -> ( ( ( ( C S A ) P B ) - ( C x. ( A P B ) ) ) = 0 <-> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) )
32 18 31 mpbid 
 |-  ( C e. RR -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) )