Metamath Proof Explorer

Theorem ipasslem5

Description: Lemma for ipassi . Show the inner product associative law for rational numbers. (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
ipasslem1.b 
|- B e. X
Assertion ipasslem5 
|- ( ( C e. QQ /\ A e. X ) -> ( ( 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 ipasslem1.b 
 |-  B e. X
7 elq 
 |-  ( C e. QQ <-> E. j e. ZZ E. k e. NN C = ( j / k ) )
8 zcn 
 |-  ( j e. ZZ -> j e. CC )
9 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
10 9 recnd 
 |-  ( k e. NN -> ( 1 / k ) e. CC )
11 5 phnvi 
 |-  U e. NrmCVec
12 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
13 11 6 12 mp3an13 
 |-  ( A e. X -> ( A P B ) e. CC )
14 mulass 
 |-  ( ( j e. CC /\ ( 1 / k ) e. CC /\ ( A P B ) e. CC ) -> ( ( j x. ( 1 / k ) ) x. ( A P B ) ) = ( j x. ( ( 1 / k ) x. ( A P B ) ) ) )
15 8 10 13 14 syl3an 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( j x. ( 1 / k ) ) x. ( A P B ) ) = ( j x. ( ( 1 / k ) x. ( A P B ) ) ) )
16 8 adantr 
 |-  ( ( j e. ZZ /\ k e. NN ) -> j e. CC )
17 nncn 
 |-  ( k e. NN -> k e. CC )
18 17 adantl 
 |-  ( ( j e. ZZ /\ k e. NN ) -> k e. CC )
19 nnne0 
 |-  ( k e. NN -> k =/= 0 )
20 19 adantl 
 |-  ( ( j e. ZZ /\ k e. NN ) -> k =/= 0 )
21 16 18 20 divrecd 
 |-  ( ( j e. ZZ /\ k e. NN ) -> ( j / k ) = ( j x. ( 1 / k ) ) )
22 21 3adant3 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( j / k ) = ( j x. ( 1 / k ) ) )
23 22 oveq1d 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( j / k ) x. ( A P B ) ) = ( ( j x. ( 1 / k ) ) x. ( A P B ) ) )
24 22 oveq1d 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( j / k ) S A ) = ( ( j x. ( 1 / k ) ) S A ) )
25 id 
 |-  ( A e. X -> A e. X )
26 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( j e. CC /\ ( 1 / k ) e. CC /\ A e. X ) ) -> ( ( j x. ( 1 / k ) ) S A ) = ( j S ( ( 1 / k ) S A ) ) )
27 11 26 mpan 
 |-  ( ( j e. CC /\ ( 1 / k ) e. CC /\ A e. X ) -> ( ( j x. ( 1 / k ) ) S A ) = ( j S ( ( 1 / k ) S A ) ) )
28 8 10 25 27 syl3an 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( j x. ( 1 / k ) ) S A ) = ( j S ( ( 1 / k ) S A ) ) )
29 24 28 eqtrd 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( j / k ) S A ) = ( j S ( ( 1 / k ) S A ) ) )
30 29 oveq1d 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( ( j / k ) S A ) P B ) = ( ( j S ( ( 1 / k ) S A ) ) P B ) )
31 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ ( 1 / k ) e. CC /\ A e. X ) -> ( ( 1 / k ) S A ) e. X )
32 11 31 mp3an1 
 |-  ( ( ( 1 / k ) e. CC /\ A e. X ) -> ( ( 1 / k ) S A ) e. X )
33 10 32 sylan 
 |-  ( ( k e. NN /\ A e. X ) -> ( ( 1 / k ) S A ) e. X )
34 1 2 3 4 5 6 ipasslem3 
 |-  ( ( j e. ZZ /\ ( ( 1 / k ) S A ) e. X ) -> ( ( j S ( ( 1 / k ) S A ) ) P B ) = ( j x. ( ( ( 1 / k ) S A ) P B ) ) )
35 33 34 sylan2 
 |-  ( ( j e. ZZ /\ ( k e. NN /\ A e. X ) ) -> ( ( j S ( ( 1 / k ) S A ) ) P B ) = ( j x. ( ( ( 1 / k ) S A ) P B ) ) )
36 35 3impb 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( j S ( ( 1 / k ) S A ) ) P B ) = ( j x. ( ( ( 1 / k ) S A ) P B ) ) )
37 1 2 3 4 5 6 ipasslem4 
 |-  ( ( k e. NN /\ A e. X ) -> ( ( ( 1 / k ) S A ) P B ) = ( ( 1 / k ) x. ( A P B ) ) )
38 37 3adant1 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( ( 1 / k ) S A ) P B ) = ( ( 1 / k ) x. ( A P B ) ) )
39 38 oveq2d 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( j x. ( ( ( 1 / k ) S A ) P B ) ) = ( j x. ( ( 1 / k ) x. ( A P B ) ) ) )
40 30 36 39 3eqtrd 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( ( j / k ) S A ) P B ) = ( j x. ( ( 1 / k ) x. ( A P B ) ) ) )
41 15 23 40 3eqtr4rd 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( ( ( j / k ) S A ) P B ) = ( ( j / k ) x. ( A P B ) ) )
42 oveq1 
 |-  ( C = ( j / k ) -> ( C S A ) = ( ( j / k ) S A ) )
43 42 oveq1d 
 |-  ( C = ( j / k ) -> ( ( C S A ) P B ) = ( ( ( j / k ) S A ) P B ) )
44 oveq1 
 |-  ( C = ( j / k ) -> ( C x. ( A P B ) ) = ( ( j / k ) x. ( A P B ) ) )
45 43 44 eqeq12d 
 |-  ( C = ( j / k ) -> ( ( ( C S A ) P B ) = ( C x. ( A P B ) ) <-> ( ( ( j / k ) S A ) P B ) = ( ( j / k ) x. ( A P B ) ) ) )
46 41 45 syl5ibrcom 
 |-  ( ( j e. ZZ /\ k e. NN /\ A e. X ) -> ( C = ( j / k ) -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) )
47 46 3expia 
 |-  ( ( j e. ZZ /\ k e. NN ) -> ( A e. X -> ( C = ( j / k ) -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) ) )
48 47 com23 
 |-  ( ( j e. ZZ /\ k e. NN ) -> ( C = ( j / k ) -> ( A e. X -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) ) )
49 48 rexlimivv 
 |-  ( E. j e. ZZ E. k e. NN C = ( j / k ) -> ( A e. X -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) )
50 7 49 sylbi 
 |-  ( C e. QQ -> ( A e. X -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) )
51 50 imp 
 |-  ( ( C e. QQ /\ A e. X ) -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) )