Theorem 0ofval

Description: The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0oval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	0oval.6	$$⊢Z=0_{\mathrm{vec}}\left(W\right)$$
	0oval.0	$$⊢O=U{0}_{\mathrm{op}}W$$
Assertion	0ofval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to O=X\times \left\{Z\right\}$$

Proof

Step	Hyp	Ref	Expression
1		0oval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		0oval.6	$$⊢Z=0_{\mathrm{vec}}\left(W\right)$$
3		0oval.0	$$⊢O=U{0}_{\mathrm{op}}W$$
4		fveq2	$$⊢u=U\to \mathrm{BaseSet}\left(u\right)=\mathrm{BaseSet}\left(U\right)$$
5	4 1	eqtr4di	$$⊢u=U\to \mathrm{BaseSet}\left(u\right)=X$$
6	5	xpeq1d	$$⊢u=U\to \mathrm{BaseSet}\left(u\right)\times \left\{0_{\mathrm{vec}}\left(w\right)\right\}=X\times \left\{0_{\mathrm{vec}}\left(w\right)\right\}$$
7		fveq2	$$⊢w=W\to 0_{\mathrm{vec}}\left(w\right)=0_{\mathrm{vec}}\left(W\right)$$
8	7 2	eqtr4di	$$⊢w=W\to 0_{\mathrm{vec}}\left(w\right)=Z$$
9	8	sneqd	$$⊢w=W\to \left\{0_{\mathrm{vec}}\left(w\right)\right\}=\left\{Z\right\}$$
10	9	xpeq2d	$$⊢w=W\to X\times \left\{0_{\mathrm{vec}}\left(w\right)\right\}=X\times \left\{Z\right\}$$
11		df-0o	$$⊢0_{\mathrm{op}}=\left(u\in \mathrm{NrmCVec},w\in \mathrm{NrmCVec}⟼\mathrm{BaseSet}\left(u\right)\times \left\{0_{\mathrm{vec}}\left(w\right)\right\}\right)$$
12	1	fvexi	$$⊢X\in \mathrm{V}$$
13		snex	$$⊢\left\{Z\right\}\in \mathrm{V}$$
14	12 13	xpex	$$⊢X\times \left\{Z\right\}\in \mathrm{V}$$
15	6 10 11 14	ovmpo	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to U{0}_{\mathrm{op}}W=X\times \left\{Z\right\}$$
16	3 15	syl5eq	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to O=X\times \left\{Z\right\}$$