Metamath Proof Explorer

Theorem ip2i

Description: Equation 6.48 of Ponnusamy p. 362. (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

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

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 ip2i.8 ⊢ 𝐴 ∈ 𝑋
7 ip2i.9 ⊢ 𝐵 ∈ 𝑋
8 5 phnvi ⊢ 𝑈 ∈ NrmCVec
9 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) ∈ 𝑋 )
10 8 6 6 9 mp3an ⊢ ( 𝐴 𝐺 𝐴 ) ∈ 𝑋
11 1 4 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 ) ∈ ℂ )
12 8 10 7 11 mp3an ⊢ ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 ) ∈ ℂ
13 12 addridi ⊢ ( ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 ) + 0 ) = ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 )
14 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
15 1 2 3 14 nvrinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
16 8 6 15 mp2an ⊢ ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) = ( 0vec ‘ 𝑈 )
17 16 oveq1i ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 )
18 1 14 4 dip0l ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0 )
19 8 7 18 mp2an ⊢ ( ( 0vec ‘ 𝑈 ) 𝑃 𝐵 ) = 0
20 17 19 eqtri ⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) = 0
21 20 oveq2i ⊢ ( ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) ) = ( ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 ) + 0 )
22 df-2 ⊢ 2 = ( 1 + 1 )
23 22 oveq1i ⊢ ( 2 𝑆 𝐴 ) = ( ( 1 + 1 ) 𝑆 𝐴 )
24 ax-1cn ⊢ 1 ∈ ℂ
25 24 24 6 3pm3.2i ⊢ ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 )
26 1 2 3 nvdir ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
27 8 25 26 mp2an ⊢ ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) )
28 1 3 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
29 8 6 28 mp2an ⊢ ( 1 𝑆 𝐴 ) = 𝐴
30 29 29 oveq12i ⊢ ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( 𝐴 𝐺 𝐴 )
31 27 30 eqtri ⊢ ( ( 1 + 1 ) 𝑆 𝐴 ) = ( 𝐴 𝐺 𝐴 )
32 23 31 eqtri ⊢ ( 2 𝑆 𝐴 ) = ( 𝐴 𝐺 𝐴 )
33 32 oveq1i ⊢ ( ( 2 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 )
34 13 21 33 3eqtr4ri ⊢ ( ( 2 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
35 1 2 3 4 5 6 6 7 ip1i ⊢ ( ( ( 𝐴 𝐺 𝐴 ) 𝑃 𝐵 ) + ( ( 𝐴 𝐺 ( - 1 𝑆 𝐴 ) ) 𝑃 𝐵 ) ) = ( 2 · ( 𝐴 𝑃 𝐵 ) )
36 34 35 eqtri ⊢ ( ( 2 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 2 · ( 𝐴 𝑃 𝐵 ) )