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

Metamath Proof Explorer

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{˙}{,} = \cdot_{𝑖} (W)$
		cphipcj.v	$⊢ V = {Base}_{W}$
	Assertion	cphorthcom	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to (A \underset{˙}{,} B = 0 \leftrightarrow B \underset{˙}{,} A = 0)$

Proof

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