This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipasslem1.b ⊢ 𝐵 ∈ 𝑋
Assertion ipasslem4 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
5 ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
6 ipasslem1.b ⊢ 𝐵 ∈ 𝑋
7 nnrecre ⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ )
8 7 recnd ⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℂ )
9 5 phnvi ⊢ 𝑈 ∈ NrmCVec
10 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 )
11 9 10 mp3an1 ⊢ ( ( ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 )
12 8 11 sylan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 )
13 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
14 9 6 13 mp3an13 ⊢ ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
15 12 14 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
16 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
17 9 6 16 mp3an13 ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
18 mulcl ⊢ ( ( ( 1 / 𝑁 ) ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
19 8 17 18 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℂ )
20 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
21 20 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝑁 ∈ ℂ )
22 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
23 22 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝑁 ≠ 0 )
24 20 22 recidd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · ( 1 / 𝑁 ) ) = 1 )
25 24 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 1 · ( 𝐴 𝑃 𝐵 ) ) )
26 17 mullidd ⊢ ( 𝐴 ∈ 𝑋 → ( 1 · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
27 25 26 sylan9eq ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝐴 𝑃 𝐵 ) )
28 24 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 1 𝑆 𝐴 ) )
29 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
30 9 29 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( 1 𝑆 𝐴 ) = 𝐴 )
31 28 30 sylan9eq ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = 𝐴 )
32 8 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 1 / 𝑁 ) ∈ ℂ )
33 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
34 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑁 ∈ ℂ ∧ ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
35 9 34 mpan ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 1 / 𝑁 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
36 21 32 33 35 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) 𝑆 𝐴 ) = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
37 31 36 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝐴 = ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) )
38 37 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) = ( ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
39 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
40 39 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝑁 ∈ ℕ0 )
41 1 2 3 4 5 6 ipasslem1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
42 40 12 41 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 𝑆 ( ( 1 / 𝑁 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
43 27 38 42 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
44 17 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
45 21 32 44 mulassd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 · ( 1 / 𝑁 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑁 · ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
46 43 45 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( 𝑁 · ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
47 15 19 21 23 46 mulcanad ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 1 / 𝑁 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 1 / 𝑁 ) · ( 𝐴 𝑃 𝐵 ) ) )