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 ( ( 𝐶 ∈ ℚ ∧ 𝐴𝑋 ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )