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=⋅𝑠OLD⁡U
ip1i.7 ⊢P=⋅𝑖OLD⁡U
ip1i.9 ⊢U∈CPreHilOLD
ipasslem1.b ⊢B∈X
Assertion ipasslem4 ⊢N∈ℕ∧A∈X→1NSAPB=1N⁢APB

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢X=BaseSet⁡U
2 ip1i.2 ⊢G=+v⁡U
3 ip1i.4 ⊢S=⋅𝑠OLD⁡U
4 ip1i.7 ⊢P=⋅𝑖OLD⁡U
5 ip1i.9 ⊢U∈CPreHilOLD
6 ipasslem1.b ⊢B∈X
7 nnrecre ⊢N∈ℕ→1N∈ℝ
8 7 recnd ⊢N∈ℕ→1N∈ℂ
9 5 phnvi ⊢U∈NrmCVec
10 1 3 nvscl ⊢U∈NrmCVec∧1N∈ℂ∧A∈X→1NSA∈X
11 9 10 mp3an1 ⊢1N∈ℂ∧A∈X→1NSA∈X
12 8 11 sylan ⊢N∈ℕ∧A∈X→1NSA∈X
13 1 4 dipcl ⊢U∈NrmCVec∧1NSA∈X∧B∈X→1NSAPB∈ℂ
14 9 6 13 mp3an13 ⊢1NSA∈X→1NSAPB∈ℂ
15 12 14 syl ⊢N∈ℕ∧A∈X→1NSAPB∈ℂ
16 1 4 dipcl ⊢U∈NrmCVec∧A∈X∧B∈X→APB∈ℂ
17 9 6 16 mp3an13 ⊢A∈X→APB∈ℂ
18 mulcl ⊢1N∈ℂ∧APB∈ℂ→1N⁢APB∈ℂ
19 8 17 18 syl2an ⊢N∈ℕ∧A∈X→1N⁢APB∈ℂ
20 nncn ⊢N∈ℕ→N∈ℂ
21 20 adantr ⊢N∈ℕ∧A∈X→N∈ℂ
22 nnne0 ⊢N∈ℕ→N≠0
23 22 adantr ⊢N∈ℕ∧A∈X→N≠0
24 20 22 recidd ⊢N∈ℕ→N⁢1N=1
25 24 oveq1d ⊢N∈ℕ→N⁢1N⁢APB=1⁢APB
26 17 mullidd ⊢A∈X→1⁢APB=APB
27 25 26 sylan9eq ⊢N∈ℕ∧A∈X→N⁢1N⁢APB=APB
28 24 oveq1d ⊢N∈ℕ→N⁢1NSA=1SA
29 1 3 nvsid ⊢U∈NrmCVec∧A∈X→1SA=A
30 9 29 mpan ⊢A∈X→1SA=A
31 28 30 sylan9eq ⊢N∈ℕ∧A∈X→N⁢1NSA=A
32 8 adantr ⊢N∈ℕ∧A∈X→1N∈ℂ
33 simpr ⊢N∈ℕ∧A∈X→A∈X
34 1 3 nvsass ⊢U∈NrmCVec∧N∈ℂ∧1N∈ℂ∧A∈X→N⁢1NSA=NS1NSA
35 9 34 mpan ⊢N∈ℂ∧1N∈ℂ∧A∈X→N⁢1NSA=NS1NSA
36 21 32 33 35 syl3anc ⊢N∈ℕ∧A∈X→N⁢1NSA=NS1NSA
37 31 36 eqtr3d ⊢N∈ℕ∧A∈X→A=NS1NSA
38 37 oveq1d ⊢N∈ℕ∧A∈X→APB=NS1NSAPB
39 nnnn0 ⊢N∈ℕ→N∈ℕ0
40 39 adantr ⊢N∈ℕ∧A∈X→N∈ℕ0
41 1 2 3 4 5 6 ipasslem1 ⊢N∈ℕ0∧1NSA∈X→NS1NSAPB=N⁢1NSAPB
42 40 12 41 syl2anc ⊢N∈ℕ∧A∈X→NS1NSAPB=N⁢1NSAPB
43 27 38 42 3eqtrd ⊢N∈ℕ∧A∈X→N⁢1N⁢APB=N⁢1NSAPB
44 17 adantl ⊢N∈ℕ∧A∈X→APB∈ℂ
45 21 32 44 mulassd ⊢N∈ℕ∧A∈X→N⁢1N⁢APB=N⁢1N⁢APB
46 43 45 eqtr3d ⊢N∈ℕ∧A∈X→N⁢1NSAPB=N⁢1N⁢APB
47 15 19 21 23 46 mulcanad ⊢N∈ℕ∧A∈X→1NSAPB=1N⁢APB