0oval

Description: Value of the zero operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0oval.1	$⊢ X = BaseSet (U)$
	0oval.6	$⊢ Z = 0_{vec} (W)$
	0oval.0	$⊢ O = U 0_{op} W$
Assertion	0oval	$⊢ (U \in NrmCVec \land W \in NrmCVec \land A \in X) \to O (A) = Z$

Step	Hyp	Ref	Expression
1		0oval.1	$⊢ X = BaseSet (U)$
2		0oval.6	$⊢ Z = 0_{vec} (W)$
3		0oval.0	$⊢ O = U 0_{op} W$
4	1 2 3	0ofval	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to O = X \times \{Z\}$
5	4	fveq1d	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to O (A) = (X \times \{Z\}) (A)$
6	5	3adant3	$⊢ (U \in NrmCVec \land W \in NrmCVec \land A \in X) \to O (A) = (X \times \{Z\}) (A)$
7	2	fvexi	$⊢ Z \in V$
8	7	fvconst2	$⊢ A \in X \to (X \times \{Z\}) (A) = Z$
9	8	3ad2ant3	$⊢ (U \in NrmCVec \land W \in NrmCVec \land A \in X) \to (X \times \{Z\}) (A) = Z$
10	6 9	eqtrd	$⊢ (U \in NrmCVec \land W \in NrmCVec \land A \in X) \to O (A) = Z$

Metamath Proof Explorer