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 ⊢ X = BaseSet ⁡ U
ip1i.2 ⊢ G = + v ⁡ U
ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip1i.9 ⊢ U ∈ CPreHil OLD
ip2i.8 ⊢ A ∈ X
ip2i.9 ⊢ B ∈ X
Assertion ip2i ⊢ 2 S A P B = 2 ⁢ 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 ip2i.8 ⊢ A ∈ X
7 ip2i.9 ⊢ B ∈ X
8 5 phnvi ⊢ U ∈ NrmCVec
9 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ∈ X → A G A ∈ X
10 8 6 6 9 mp3an ⊢ A G A ∈ X
11 1 4 dipcl ⊢ U ∈ NrmCVec ∧ A G A ∈ X ∧ B ∈ X → A G A P B ∈ ℂ
12 8 10 7 11 mp3an ⊢ A G A P B ∈ ℂ
13 12 addid1i ⊢ A G A P B + 0 = A G A P B
14 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
15 1 2 3 14 nvrinv ⊢ U ∈ NrmCVec ∧ A ∈ X → A G -1 S A = 0 vec ⁡ U
16 8 6 15 mp2an ⊢ A G -1 S A = 0 vec ⁡ U
17 16 oveq1i ⊢ A G -1 S A P B = 0 vec ⁡ U P B
18 1 14 4 dip0l ⊢ U ∈ NrmCVec ∧ B ∈ X → 0 vec ⁡ U P B = 0
19 8 7 18 mp2an ⊢ 0 vec ⁡ U P B = 0
20 17 19 eqtri ⊢ A G -1 S A P B = 0
21 20 oveq2i ⊢ A G A P B + A G -1 S A P B = A G A P B + 0
22 df-2 ⊢ 2 = 1 + 1
23 22 oveq1i ⊢ 2 S A = 1 + 1 S A
24 ax-1cn ⊢ 1 ∈ ℂ
25 24 24 6 3pm3.2i ⊢ 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ A ∈ X
26 1 2 3 nvdir ⊢ U ∈ NrmCVec ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ A ∈ X → 1 + 1 S A = 1 S A G 1 S A
27 8 25 26 mp2an ⊢ 1 + 1 S A = 1 S A G 1 S A
28 1 3 nvsid ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 S A = A
29 8 6 28 mp2an ⊢ 1 S A = A
30 29 29 oveq12i ⊢ 1 S A G 1 S A = A G A
31 27 30 eqtri ⊢ 1 + 1 S A = A G A
32 23 31 eqtri ⊢ 2 S A = A G A
33 32 oveq1i ⊢ 2 S A P B = A G A P B
34 13 21 33 3eqtr4ri ⊢ 2 S A P B = A G A P B + A G -1 S A P B
35 1 2 3 4 5 6 6 7 ip1i ⊢ A G A P B + A G -1 S A P B = 2 ⁢ A P B
36 34 35 eqtri ⊢ 2 S A P B = 2 ⁢ A P B