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

Metamath Proof Explorer

Theorem cphipeq0

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. Complex version of ipeq0 . (Contributed by Mario Carneiro, 16-Oct-2015)

		Ref	Expression
	Hypotheses	cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
		cphipcj.v	$⊢ V = {Base}_{W}$
		cphip0l.z	$⊢ \underset{˙}{0} = 0_{W}$
	Assertion	cphipeq0	$⊢ (W \in CPreHil \land A \in V) \to (A \underset{˙}{,} A = 0 \leftrightarrow A = \underset{˙}{0})$

Proof

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