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 ) )