Theorem cphorthcom

Description: Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	cphipcj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion	cphorthcom	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = 0 ↔ ( 𝐵 , 𝐴 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
2		cphipcj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		cphphl	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
4		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
6	4 1 2 5	iporthcom	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝐵 , 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
7	3 6	syl3an1	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝐵 , 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
8		cphclm	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
9	4	clm0	⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
10	8 9	syl	⊢ ( 𝑊 ∈ ℂPreHil → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
11	10	3ad2ant1	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
12	11	eqeq2d	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = 0 ↔ ( 𝐴 , 𝐵 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
13	11	eqeq2d	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐵 , 𝐴 ) = 0 ↔ ( 𝐵 , 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
14	7 12 13	3bitr4d	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = 0 ↔ ( 𝐵 , 𝐴 ) = 0 ) )