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

Metamath Proof Explorer

Theorem ip1i

Description: Equation 6.47 of Ponnusamy p. 362. (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
ip1i.a ⊢ A ∈ X
ip1i.b ⊢ B ∈ X
ip1i.c ⊢ C ∈ X
Assertion ip1i ⊢ A G B P C + A G -1 S B P C = 2 ⁢ A P C

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 ip1i.a ⊢ A ∈ X
7 ip1i.b ⊢ B ∈ X
8 ip1i.c ⊢ C ∈ X
9 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
10 ax-1cn ⊢ 1 ∈ ℂ
11 1 2 3 4 5 6 7 8 9 10 ip1ilem ⊢ A G B P C + A G -1 S B P C = 2 ⁢ A P C