0oo

Description: The zero operator is an operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0oo.1	$⊢ X = BaseSet (U)$
	0oo.2	$⊢ Y = BaseSet (W)$
	0oo.0	$⊢ Z = U 0_{op} W$
Assertion	0oo	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z : X ⟶ Y$

Step	Hyp	Ref	Expression
1		0oo.1	$⊢ X = BaseSet (U)$
2		0oo.2	$⊢ Y = BaseSet (W)$
3		0oo.0	$⊢ Z = U 0_{op} W$
4		fvex	$⊢ 0_{vec} (W) \in V$
5	4	fconst	$⊢ (X \times \{0_{vec} (W)\}) : X ⟶ \{0_{vec} (W)\}$
6		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
7	2 6	nvzcl	$⊢ W \in NrmCVec \to 0_{vec} (W) \in Y$
8	7	snssd	$⊢ W \in NrmCVec \to \{0_{vec} (W)\} \subseteq Y$
9		fss	$⊢ ((X \times \{0_{vec} (W)\}) : X ⟶ \{0_{vec} (W)\} \land \{0_{vec} (W)\} \subseteq Y) \to (X \times \{0_{vec} (W)\}) : X ⟶ Y$
10	5 8 9	sylancr	$⊢ W \in NrmCVec \to (X \times \{0_{vec} (W)\}) : X ⟶ Y$
11	10	adantl	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (X \times \{0_{vec} (W)\}) : X ⟶ Y$
12	1 6 3	0ofval	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z = X \times \{0_{vec} (W)\}$
13	12	feq1d	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (Z : X ⟶ Y \leftrightarrow (X \times \{0_{vec} (W)\}) : X ⟶ Y)$
14	11 13	mpbird	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z : X ⟶ Y$

Metamath Proof Explorer