Metamath Proof Explorer

Theorem ipz

Description: The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of Kreyszig p. 129. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	dip0r.1	$⊢ X = BaseSet (U)$
		dip0r.5	$⊢ Z = 0_{vec} (U)$
		dip0r.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	Assertion	ipz	$⊢ (U \in NrmCVec \land A \in X) \to (A P A = 0 \leftrightarrow A = Z)$

Proof

Step	Hyp	Ref	Expression
1		dip0r.1	$⊢ X = BaseSet (U)$
2		dip0r.5	$⊢ Z = 0_{vec} (U)$
3		dip0r.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
5	1 4 3	ipidsq	$⊢ (U \in NrmCVec \land A \in X) \to A P A = {{norm}_{CV} (U) (A)}^{2}$
6	5	eqeq1d	$⊢ (U \in NrmCVec \land A \in X) \to (A P A = 0 \leftrightarrow {{norm}_{CV} (U) (A)}^{2} = 0)$
7	1 4	nvcl	$⊢ (U \in NrmCVec \land A \in X) \to {norm}_{CV} (U) (A) \in ℝ$
8	7	recnd	$⊢ (U \in NrmCVec \land A \in X) \to {norm}_{CV} (U) (A) \in ℂ$
9		sqeq0	$⊢ {norm}_{CV} (U) (A) \in ℂ \to ({{norm}_{CV} (U) (A)}^{2} = 0 \leftrightarrow {norm}_{CV} (U) (A) = 0)$
10	8 9	syl	$⊢ (U \in NrmCVec \land A \in X) \to ({{norm}_{CV} (U) (A)}^{2} = 0 \leftrightarrow {norm}_{CV} (U) (A) = 0)$
11	1 2 4	nvz	$⊢ (U \in NrmCVec \land A \in X) \to ({norm}_{CV} (U) (A) = 0 \leftrightarrow A = Z)$
12	6 10 11	3bitrd	$⊢ (U \in NrmCVec \land A \in X) \to (A P A = 0 \leftrightarrow A = Z)$