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 ⊢ X = BaseSet ⁡ U
ip1i.2 ⊢ G = + v ⁡ U
ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip1i.9 ⊢ U ∈ CPreHil OLD
ipasslem1.b ⊢ B ∈ X
Assertion ipasslem5 ⊢ C ∈ ℚ ∧ A ∈ X → C S A P B = C ⁢ A P B

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 ∈ CPreHil OLD
6 ipasslem1.b ⊢ B ∈ X
7 elq ⊢ C ∈ ℚ ↔ ∃ j ∈ ℤ ∃ k ∈ ℕ C = j k
8 zcn ⊢ j ∈ ℤ → j ∈ ℂ
9 nnrecre ⊢ k ∈ ℕ → 1 k ∈ ℝ
10 9 recnd ⊢ k ∈ ℕ → 1 k ∈ ℂ
11 5 phnvi ⊢ U ∈ NrmCVec
12 1 4 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ∈ ℂ
13 11 6 12 mp3an13 ⊢ A ∈ X → A P B ∈ ℂ
14 mulass ⊢ j ∈ ℂ ∧ 1 k ∈ ℂ ∧ A P B ∈ ℂ → j ⁢ 1 k ⁢ A P B = j ⁢ 1 k ⁢ A P B
15 8 10 13 14 syl3an ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j ⁢ 1 k ⁢ A P B = j ⁢ 1 k ⁢ A P B
16 8 adantr ⊢ j ∈ ℤ ∧ k ∈ ℕ → j ∈ ℂ
17 nncn ⊢ k ∈ ℕ → k ∈ ℂ
18 17 adantl ⊢ j ∈ ℤ ∧ k ∈ ℕ → k ∈ ℂ
19 nnne0 ⊢ k ∈ ℕ → k ≠ 0
20 19 adantl ⊢ j ∈ ℤ ∧ k ∈ ℕ → k ≠ 0
21 16 18 20 divrecd ⊢ j ∈ ℤ ∧ k ∈ ℕ → j k = j ⁢ 1 k
22 21 3adant3 ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j k = j ⁢ 1 k
23 22 oveq1d ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j k ⁢ A P B = j ⁢ 1 k ⁢ A P B
24 22 oveq1d ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j k S A = j ⁢ 1 k S A
25 id ⊢ A ∈ X → A ∈ X
26 1 3 nvsass ⊢ U ∈ NrmCVec ∧ j ∈ ℂ ∧ 1 k ∈ ℂ ∧ A ∈ X → j ⁢ 1 k S A = j S 1 k S A
27 11 26 mpan ⊢ j ∈ ℂ ∧ 1 k ∈ ℂ ∧ A ∈ X → j ⁢ 1 k S A = j S 1 k S A
28 8 10 25 27 syl3an ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j ⁢ 1 k S A = j S 1 k S A
29 24 28 eqtrd ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j k S A = j S 1 k S A
30 29 oveq1d ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j k S A P B = j S 1 k S A P B
31 1 3 nvscl ⊢ U ∈ NrmCVec ∧ 1 k ∈ ℂ ∧ A ∈ X → 1 k S A ∈ X
32 11 31 mp3an1 ⊢ 1 k ∈ ℂ ∧ A ∈ X → 1 k S A ∈ X
33 10 32 sylan ⊢ k ∈ ℕ ∧ A ∈ X → 1 k S A ∈ X
34 1 2 3 4 5 6 ipasslem3 ⊢ j ∈ ℤ ∧ 1 k S A ∈ X → j S 1 k S A P B = j ⁢ 1 k S A P B
35 33 34 sylan2 ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j S 1 k S A P B = j ⁢ 1 k S A P B
36 35 3impb ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j S 1 k S A P B = j ⁢ 1 k S A P B
37 1 2 3 4 5 6 ipasslem4 ⊢ k ∈ ℕ ∧ A ∈ X → 1 k S A P B = 1 k ⁢ A P B
38 37 3adant1 ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → 1 k S A P B = 1 k ⁢ A P B
39 38 oveq2d ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j ⁢ 1 k S A P B = j ⁢ 1 k ⁢ A P B
40 30 36 39 3eqtrd ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j k S A P B = j ⁢ 1 k ⁢ A P B
41 15 23 40 3eqtr4rd ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → j k S A P B = j k ⁢ A P B
42 oveq1 ⊢ C = j k → C S A = j k S A
43 42 oveq1d ⊢ C = j k → C S A P B = j k S A P B
44 oveq1 ⊢ C = j k → C ⁢ A P B = j k ⁢ A P B
45 43 44 eqeq12d ⊢ C = j k → C S A P B = C ⁢ A P B ↔ j k S A P B = j k ⁢ A P B
46 41 45 syl5ibrcom ⊢ j ∈ ℤ ∧ k ∈ ℕ ∧ A ∈ X → C = j k → C S A P B = C ⁢ A P B
47 46 3expia ⊢ j ∈ ℤ ∧ k ∈ ℕ → A ∈ X → C = j k → C S A P B = C ⁢ A P B
48 47 com23 ⊢ j ∈ ℤ ∧ k ∈ ℕ → C = j k → A ∈ X → C S A P B = C ⁢ A P B
49 48 rexlimivv ⊢ ∃ j ∈ ℤ ∃ k ∈ ℕ C = j k → A ∈ X → C S A P B = C ⁢ A P B
50 7 49 sylbi ⊢ C ∈ ℚ → A ∈ X → C S A P B = C ⁢ A P B
51 50 imp ⊢ C ∈ ℚ ∧ A ∈ X → C S A P B = C ⁢ A P B