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

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 elq ⊢ ( 𝐶 ∈ ℚ ↔ ∃ 𝑗 ∈ ℤ ∃ 𝑘 ∈ ℕ 𝐶 = ( 𝑗 / 𝑘 ) )
8 zcn ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℂ )
9 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
10 9 recnd ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℂ )
11 5 phnvi ⊢ 𝑈 ∈ NrmCVec
12 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
13 11 6 12 mp3an13 ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
14 mulass ⊢ ( ( 𝑗 ∈ ℂ ∧ ( 1 / 𝑘 ) ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑗 · ( 1 / 𝑘 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑗 · ( ( 1 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
15 8 10 13 14 syl3an ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑗 · ( 1 / 𝑘 ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑗 · ( ( 1 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
16 8 adantr ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → 𝑗 ∈ ℂ )
17 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
18 17 adantl ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
19 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
20 19 adantl ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ≠ 0 )
21 16 18 20 divrecd ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( 𝑗 / 𝑘 ) = ( 𝑗 · ( 1 / 𝑘 ) ) )
22 21 3adant3 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑗 / 𝑘 ) = ( 𝑗 · ( 1 / 𝑘 ) ) )
23 22 oveq1d ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑗 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑗 · ( 1 / 𝑘 ) ) · ( 𝐴 𝑃 𝐵 ) ) )
24 22 oveq1d ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) = ( ( 𝑗 · ( 1 / 𝑘 ) ) 𝑆 𝐴 ) )
25 id ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ 𝑋 )
26 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑗 ∈ ℂ ∧ ( 1 / 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑗 · ( 1 / 𝑘 ) ) 𝑆 𝐴 ) = ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) )
27 11 26 mpan ⊢ ( ( 𝑗 ∈ ℂ ∧ ( 1 / 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑗 · ( 1 / 𝑘 ) ) 𝑆 𝐴 ) = ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) )
28 8 10 25 27 syl3an ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑗 · ( 1 / 𝑘 ) ) 𝑆 𝐴 ) = ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) )
29 24 28 eqtrd ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) = ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) )
30 29 oveq1d ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
31 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ∈ 𝑋 )
32 11 31 mp3an1 ⊢ ( ( ( 1 / 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ∈ 𝑋 )
33 10 32 sylan ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ∈ 𝑋 )
34 1 2 3 4 5 6 ipasslem3 ⊢ ( ( 𝑗 ∈ ℤ ∧ ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑗 · ( ( ( 1 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
35 33 34 sylan2 ⊢ ( ( 𝑗 ∈ ℤ ∧ ( 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑗 · ( ( ( 1 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
36 35 3impb ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑗 𝑆 ( ( 1 / 𝑘 ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑗 · ( ( ( 1 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
37 1 2 3 4 5 6 ipasslem4 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 1 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 1 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) )
38 37 3adant1 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 1 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 1 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) )
39 38 oveq2d ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑗 · ( ( ( 1 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( 𝑗 · ( ( 1 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
40 30 36 39 3eqtrd ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑗 · ( ( 1 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
41 15 23 40 3eqtr4rd ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑗 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) )
42 oveq1 ⊢ ( 𝐶 = ( 𝑗 / 𝑘 ) → ( 𝐶 𝑆 𝐴 ) = ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) )
43 42 oveq1d ⊢ ( 𝐶 = ( 𝑗 / 𝑘 ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) )
44 oveq1 ⊢ ( 𝐶 = ( 𝑗 / 𝑘 ) → ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑗 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) )
45 43 44 eqeq12d ⊢ ( 𝐶 = ( 𝑗 / 𝑘 ) → ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( ( 𝑗 / 𝑘 ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑗 / 𝑘 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
46 41 45 syl5ibrcom ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝐶 = ( 𝑗 / 𝑘 ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
47 46 3expia ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ∈ 𝑋 → ( 𝐶 = ( 𝑗 / 𝑘 ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
48 47 com23 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( 𝐶 = ( 𝑗 / 𝑘 ) → ( 𝐴 ∈ 𝑋 → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) ) )
49 48 rexlimivv ⊢ ( ∃ 𝑗 ∈ ℤ ∃ 𝑘 ∈ ℕ 𝐶 = ( 𝑗 / 𝑘 ) → ( 𝐴 ∈ 𝑋 → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
50 7 49 sylbi ⊢ ( 𝐶 ∈ ℚ → ( 𝐴 ∈ 𝑋 → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
51 50 imp ⊢ ( ( 𝐶 ∈ ℚ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )