diporthcom

Description: Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipcl.1	$⊢ X = BaseSet (U)$
	ipcl.7	$⊢ P = \cdot_{𝑖OLD} (U)$
Assertion	diporthcom	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A P B = 0 \leftrightarrow B P A = 0)$

Step	Hyp	Ref	Expression
1		ipcl.1	$⊢ X = BaseSet (U)$
2		ipcl.7	$⊢ P = \cdot_{𝑖OLD} (U)$
3		fveq2	$⊢ A P B = 0 \to \overline{A P B} = \overline{0}$
4		cj0	$⊢ \overline{0} = 0$
5	3 4	eqtrdi	$⊢ A P B = 0 \to \overline{A P B} = 0$
6	1 2	dipcj	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \overline{A P B} = B P A$
7	6	eqeq1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (\overline{A P B} = 0 \leftrightarrow B P A = 0)$
8	5 7	imbitrid	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A P B = 0 \to B P A = 0)$
9		fveq2	$⊢ B P A = 0 \to \overline{B P A} = \overline{0}$
10	9 4	eqtrdi	$⊢ B P A = 0 \to \overline{B P A} = 0$
11	1 2	dipcj	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to \overline{B P A} = A P B$
12	11	3com23	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \overline{B P A} = A P B$
13	12	eqeq1d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (\overline{B P A} = 0 \leftrightarrow A P B = 0)$
14	10 13	imbitrid	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (B P A = 0 \to A P B = 0)$
15	8 14	impbid	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A P B = 0 \leftrightarrow B P A = 0)$

Metamath Proof Explorer