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

Metamath Proof Explorer

Theorem cphipipcj

Description: An inner product times its conjugate. (Contributed by NM, 23-Nov-2007) (Revised by AV, 19-Oct-2021)

Ref Expression
Hypotheses cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion cphipipcj ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) · ( 𝐵 , 𝐴 ) ) = ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
2 cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 2 1 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ℂ )
4 absval ⊢ ( ( 𝐴 , 𝐵 ) ∈ ℂ → ( abs ‘ ( 𝐴 , 𝐵 ) ) = ( √ ‘ ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) ) )
5 3 4 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( abs ‘ ( 𝐴 , 𝐵 ) ) = ( √ ‘ ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) ) )
6 5 oveq1d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) = ( ( √ ‘ ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) ) ↑ 2 ) )
7 3 cjcld ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ∈ ℂ )
8 3 7 mulcld ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) ∈ ℂ )
9 8 sqsqrtd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( √ ‘ ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) ) ↑ 2 ) = ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) )
10 1 2 cphipcj ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∗ ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) )
11 10 oveq2d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) = ( ( 𝐴 , 𝐵 ) · ( 𝐵 , 𝐴 ) ) )
12 6 9 11 3eqtrrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) · ( 𝐵 , 𝐴 ) ) = ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) )