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	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	cphorthcom	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=0\leftrightarrow B\underset{\dot{}}{,}A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
3		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
4		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
5		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
6	4 1 2 5	iporthcom	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow B\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}\right)$$
7	3 6	syl3an1	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow B\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}\right)$$
8		cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$
9	4	clm0	$$⊢W\in \mathrm{CMod}\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
10	8 9	syl	$$⊢W\in \mathrm{CPreHil}\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
11	10	3ad2ant1	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
12	11	eqeq2d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=0\leftrightarrow A\underset{\dot{}}{,}B=0_{\mathrm{Scalar}\left(W\right)}\right)$$
13	11	eqeq2d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \left(B\underset{\dot{}}{,}A=0\leftrightarrow B\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}\right)$$
14	7 12 13	3bitr4d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=0\leftrightarrow B\underset{\dot{}}{,}A=0\right)$$