nmlno0

Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmlno0.3	$⊢ N = U {normOp}_{OLD} W$
	nmlno0.0	$⊢ Z = U 0_{op} W$
	nmlno0.7	$⊢ L = U LnOp W$
Assertion	nmlno0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to (N (T) = 0 \leftrightarrow T = Z)$

Proof

Step	Hyp	Ref	Expression
1		nmlno0.3	$⊢ N = U {normOp}_{OLD} W$
2		nmlno0.0	$⊢ Z = U 0_{op} W$
3		nmlno0.7	$⊢ L = U LnOp W$
4		oveq1	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to U LnOp W = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp W$
5	3 4	eqtrid	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to L = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp W$
6	5	eleq2d	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to (T \in L \leftrightarrow T \in (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp W))$
7		oveq1	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to U {normOp}_{OLD} W = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W$
8	1 7	eqtrid	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to N = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W$
9	8	fveq1d	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to N (T) = (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T)$
10	9	eqeq1d	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to (N (T) = 0 \leftrightarrow (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T) = 0)$
11		oveq1	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to U 0_{op} W = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W$
12	2 11	eqtrid	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to Z = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W$
13	12	eqeq2d	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to (T = Z \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W)$
14	10 13	bibi12d	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to ((N (T) = 0 \leftrightarrow T = Z) \leftrightarrow ((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T) = 0 \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W))$
15	6 14	imbi12d	$⊢ U = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \to ((T \in L \to (N (T) = 0 \leftrightarrow T = Z)) \leftrightarrow (T \in (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp W) \to ((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T) = 0 \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W)))$
16		oveq2	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp W = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
17	16	eleq2d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (T \in (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp W) \leftrightarrow T \in (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)))$
18		oveq2	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
19	18	fveq1d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T) = (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (T)$
20	19	eqeq1d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to ((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T) = 0 \leftrightarrow (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (T) = 0)$
21		oveq2	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
22	21	eqeq2d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩))$
23	20 22	bibi12d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T) = 0 \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W) \leftrightarrow ((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (T) = 0 \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)))$
24	17 23	imbi12d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to ((T \in (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp W) \to ((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (T) = 0 \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} W)) \leftrightarrow (T \in (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) \to ((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (T) = 0 \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩))))$
25		eqid	$⊢ if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
26		eqid	$⊢ if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
27		eqid	$⊢ if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
28		elimnvu	$⊢ if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) \in NrmCVec$
29		elimnvu	$⊢ if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \in NrmCVec$
30	25 26 27 28 29	nmlno0i	$⊢ T \in (if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) LnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) \to ((if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (T) = 0 \leftrightarrow T = if (U \in NrmCVec, U, ⟨⟨+ \times⟩, abs⟩) 0_{op} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩))$
31	15 24 30	dedth2h	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (T \in L \to (N (T) = 0 \leftrightarrow T = Z))$
32	31	3impia	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to (N (T) = 0 \leftrightarrow T = Z)$

Metamath Proof Explorer

Theorem nmlno0

Proof