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

Metamath Proof Explorer

Theorem ipipcj

Description: An inner product times its conjugate. (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1 ⊢ X = BaseSet ⁡ U
ipcl.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion ipipcj ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ⁢ B P A = A P B 2

Proof

Step Hyp Ref Expression
1 ipcl.1 ⊢ X = BaseSet ⁡ U
2 ipcl.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
3 1 2 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ∈ ℂ
4 3 absvalsqd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B 2 = A P B ⁢ A P B ‾
5 1 2 dipcj ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ‾ = B P A
6 5 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ⁢ A P B ‾ = A P B ⁢ B P A
7 4 6 eqtr2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ⁢ B P A = A P B 2