Metamath Proof Explorer

Theorem dip0l

Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of Ponnusamy p. 361. (Contributed by NM, 5-Feb-2007) (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	dip0l	$⊢ (U \in NrmCVec \land A \in X) \to Z P A = 0$

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	1 2	nvzcl	$⊢ U \in NrmCVec \to Z \in X$
5	4	adantr	$⊢ (U \in NrmCVec \land A \in X) \to Z \in X$
6	1 3	dipcj	$⊢ (U \in NrmCVec \land A \in X \land Z \in X) \to \overline{A P Z} = Z P A$
7	5 6	mpd3an3	$⊢ (U \in NrmCVec \land A \in X) \to \overline{A P Z} = Z P A$
8	1 2 3	dip0r	$⊢ (U \in NrmCVec \land A \in X) \to A P Z = 0$
9	8	fveq2d	$⊢ (U \in NrmCVec \land A \in X) \to \overline{A P Z} = \overline{0}$
10		cj0	$⊢ \overline{0} = 0$
11	9 10	eqtrdi	$⊢ (U \in NrmCVec \land A \in X) \to \overline{A P Z} = 0$
12	7 11	eqtr3d	$⊢ (U \in NrmCVec \land A \in X) \to Z P A = 0$