Metamath Proof Explorer

Theorem ipasslem4

Description: Lemma for ipassi . Show the inner product associative law for positive integer reciprocals. (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 ipasslem4 
|- ( ( N e. NN /\ A e. X ) -> ( ( ( 1 / N ) S A ) P B ) = ( ( 1 / N ) 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 nnrecre 
 |-  ( N e. NN -> ( 1 / N ) e. RR )
8 7 recnd 
 |-  ( N e. NN -> ( 1 / N ) e. CC )
9 5 phnvi 
 |-  U e. NrmCVec
10 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ ( 1 / N ) e. CC /\ A e. X ) -> ( ( 1 / N ) S A ) e. X )
11 9 10 mp3an1 
 |-  ( ( ( 1 / N ) e. CC /\ A e. X ) -> ( ( 1 / N ) S A ) e. X )
12 8 11 sylan 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( 1 / N ) S A ) e. X )
13 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ ( ( 1 / N ) S A ) e. X /\ B e. X ) -> ( ( ( 1 / N ) S A ) P B ) e. CC )
14 9 6 13 mp3an13 
 |-  ( ( ( 1 / N ) S A ) e. X -> ( ( ( 1 / N ) S A ) P B ) e. CC )
15 12 14 syl 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( ( 1 / N ) S A ) P B ) e. CC )
16 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
17 9 6 16 mp3an13 
 |-  ( A e. X -> ( A P B ) e. CC )
18 mulcl 
 |-  ( ( ( 1 / N ) e. CC /\ ( A P B ) e. CC ) -> ( ( 1 / N ) x. ( A P B ) ) e. CC )
19 8 17 18 syl2an 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( 1 / N ) x. ( A P B ) ) e. CC )
20 nncn 
 |-  ( N e. NN -> N e. CC )
21 20 adantr 
 |-  ( ( N e. NN /\ A e. X ) -> N e. CC )
22 nnne0 
 |-  ( N e. NN -> N =/= 0 )
23 22 adantr 
 |-  ( ( N e. NN /\ A e. X ) -> N =/= 0 )
24 20 22 recidd 
 |-  ( N e. NN -> ( N x. ( 1 / N ) ) = 1 )
25 24 oveq1d 
 |-  ( N e. NN -> ( ( N x. ( 1 / N ) ) x. ( A P B ) ) = ( 1 x. ( A P B ) ) )
26 17 mulid2d 
 |-  ( A e. X -> ( 1 x. ( A P B ) ) = ( A P B ) )
27 25 26 sylan9eq 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( N x. ( 1 / N ) ) x. ( A P B ) ) = ( A P B ) )
28 24 oveq1d 
 |-  ( N e. NN -> ( ( N x. ( 1 / N ) ) S A ) = ( 1 S A ) )
29 1 3 nvsid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )
30 9 29 mpan 
 |-  ( A e. X -> ( 1 S A ) = A )
31 28 30 sylan9eq 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( N x. ( 1 / N ) ) S A ) = A )
32 8 adantr 
 |-  ( ( N e. NN /\ A e. X ) -> ( 1 / N ) e. CC )
33 simpr 
 |-  ( ( N e. NN /\ A e. X ) -> A e. X )
34 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( N e. CC /\ ( 1 / N ) e. CC /\ A e. X ) ) -> ( ( N x. ( 1 / N ) ) S A ) = ( N S ( ( 1 / N ) S A ) ) )
35 9 34 mpan 
 |-  ( ( N e. CC /\ ( 1 / N ) e. CC /\ A e. X ) -> ( ( N x. ( 1 / N ) ) S A ) = ( N S ( ( 1 / N ) S A ) ) )
36 21 32 33 35 syl3anc 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( N x. ( 1 / N ) ) S A ) = ( N S ( ( 1 / N ) S A ) ) )
37 31 36 eqtr3d 
 |-  ( ( N e. NN /\ A e. X ) -> A = ( N S ( ( 1 / N ) S A ) ) )
38 37 oveq1d 
 |-  ( ( N e. NN /\ A e. X ) -> ( A P B ) = ( ( N S ( ( 1 / N ) S A ) ) P B ) )
39 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
40 39 adantr 
 |-  ( ( N e. NN /\ A e. X ) -> N e. NN0 )
41 1 2 3 4 5 6 ipasslem1 
 |-  ( ( N e. NN0 /\ ( ( 1 / N ) S A ) e. X ) -> ( ( N S ( ( 1 / N ) S A ) ) P B ) = ( N x. ( ( ( 1 / N ) S A ) P B ) ) )
42 40 12 41 syl2anc 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( N S ( ( 1 / N ) S A ) ) P B ) = ( N x. ( ( ( 1 / N ) S A ) P B ) ) )
43 27 38 42 3eqtrd 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( N x. ( 1 / N ) ) x. ( A P B ) ) = ( N x. ( ( ( 1 / N ) S A ) P B ) ) )
44 17 adantl 
 |-  ( ( N e. NN /\ A e. X ) -> ( A P B ) e. CC )
45 21 32 44 mulassd 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( N x. ( 1 / N ) ) x. ( A P B ) ) = ( N x. ( ( 1 / N ) x. ( A P B ) ) ) )
46 43 45 eqtr3d 
 |-  ( ( N e. NN /\ A e. X ) -> ( N x. ( ( ( 1 / N ) S A ) P B ) ) = ( N x. ( ( 1 / N ) x. ( A P B ) ) ) )
47 15 19 21 23 46 mulcanad 
 |-  ( ( N e. NN /\ A e. X ) -> ( ( ( 1 / N ) S A ) P B ) = ( ( 1 / N ) x. ( A P B ) ) )