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

Metamath Proof Explorer

Theorem ipasslem11

Description: Lemma for ipassi . Show the inner product associative law for all complex numbers. (Contributed by NM, 25-Aug-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
ipasslem11.a ⊢ 𝐴 ∈ 𝑋
ipasslem11.b ⊢ 𝐵 ∈ 𝑋
Assertion ipasslem11 ( 𝐶 ∈ ℂ → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )

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 ipasslem11.a ⊢ 𝐴 ∈ 𝑋
7 ipasslem11.b ⊢ 𝐵 ∈ 𝑋
8 cnre ⊢ ( 𝐶 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) )
9 ax-icn ⊢ i ∈ ℂ
10 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
11 mulcom ⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) = ( 𝑦 · i ) )
12 9 10 11 sylancr ⊢ ( 𝑦 ∈ ℝ → ( i · 𝑦 ) = ( 𝑦 · i ) )
13 12 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · 𝑦 ) = ( 𝑦 · i ) )
14 13 oveq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑥 + ( 𝑦 · i ) ) )
15 14 eqeq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) ) )
16 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
17 5 phnvi ⊢ 𝑈 ∈ NrmCVec
18 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
19 17 6 18 mp3an13 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
20 16 19 syl ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
21 mulcl ⊢ ( ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ) → ( 𝑦 · i ) ∈ ℂ )
22 10 9 21 sylancl ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 · i ) ∈ ℂ )
23 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 · i ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 )
24 17 6 23 mp3an13 ⊢ ( ( 𝑦 · i ) ∈ ℂ → ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 )
25 22 24 syl ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 )
26 1 2 3 4 5 ipdiri ⊢ ( ( ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 ∧ ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
27 7 26 mp3an3 ⊢ ( ( ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 ∧ ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
28 20 25 27 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
29 1 2 3 4 5 6 7 ipasslem9 ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) )
30 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( i 𝑆 𝐴 ) ∈ 𝑋 )
31 17 9 6 30 mp3an ⊢ ( i 𝑆 𝐴 ) ∈ 𝑋
32 1 2 3 4 5 31 7 ipasslem9 ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑦 · ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
33 1 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
34 17 33 mpan ⊢ ( ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
35 9 6 34 mp3an23 ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
36 10 35 syl ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
37 36 oveq1d ⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
38 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
39 17 6 7 38 mp3an ⊢ ( 𝐴 𝑃 𝐵 ) ∈ ℂ
40 mulass ⊢ ( ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) ) )
41 9 39 40 mp3an23 ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) ) )
42 10 41 syl ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) ) )
43 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
44 1 2 3 4 5 6 7 43 ipasslem10 ⊢ ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) = ( i · ( 𝐴 𝑃 𝐵 ) )
45 44 oveq2i ⊢ ( 𝑦 · ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) )
46 42 45 eqtr4di ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
47 32 37 46 3eqtr4d ⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) )
48 29 47 oveqan12d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
49 28 48 eqtrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
50 1 2 3 nvdir ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
51 17 50 mpan ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
52 6 51 mp3an3 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
53 16 22 52 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
54 53 oveq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
55 adddir ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
56 39 55 mp3an3 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ) → ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
57 16 22 56 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
58 49 54 57 3eqtr4d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) )
59 oveq1 ⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( 𝐶 𝑆 𝐴 ) = ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) )
60 59 oveq1d ⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) )
61 oveq1 ⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) )
62 60 61 eqeq12d ⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) ) )
63 58 62 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
64 15 63 sylbid ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
65 64 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )
66 8 65 syl ⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )