Theorem nmlno0 8455

Description: The norm of a linear operator is zero iff the operator is zero.

Hypotheses

Ref	Expression
nmlno0.3	|- N = (UnormOpW)
nmlno0.0	|- Z = (U 0op W)
nmlno0.7	|- L = (U LnOp W)

Assertion

Ref	Expression
nmlno0	|- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> ((N` T) = 0 <-> T = Z))

Proof of Theorem nmlno0

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . . 6 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> (U LnOp W) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp W))
2		nmlno0.7	. . . . . 6 |- L = (U LnOp W)
3	1, 2	syl5eq 1519	. . . . 5 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> L = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp W))
4	3	eleq2d 1541	. . . 4 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> (T e. L <-> T e. (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp W)))
5		opreq1 3968	. . . . . . . 8 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> (UnormOpW) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW))
6		nmlno0.3	. . . . . . . 8 |- N = (UnormOpW)
7	5, 6	syl5eq 1519	. . . . . . 7 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> N = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW))
8	7	fveq1d 3726	. . . . . 6 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> (N` T) = ((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T))
9	8	eqeq1d 1483	. . . . 5 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> ((N` T) = 0 <-> ((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T) = 0))
10		opreq1 3968	. . . . . . 7 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> (U 0op W) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W))
11		nmlno0.0	. . . . . . 7 |- Z = (U 0op W)
12	10, 11	syl5eq 1519	. . . . . 6 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> Z = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W))
13	12	eqeq2d 1486	. . . . 5 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> (T = Z <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W)))
14	9, 13	bibi12d 629	. . . 4 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> (((N` T) = 0 <-> T = Z) <-> (((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T) = 0 <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W))))
15	4, 14	imbi12d 626	. . 3 |- (U = if(U e. NrmCVec, U, <.<. + , x. >., abs>.) -> ((T e. L -> ((N` T) = 0 <-> T = Z)) <-> (T e. (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp W) -> (((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T) = 0 <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W)))))
16		opreq2 3969	. . . . 5 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp W) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp if(W e. NrmCVec, W, <.<. + , x. >., abs>.)))
17	16	eleq2d 1541	. . . 4 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> (T e. (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp W) <-> T e. (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp if(W e. NrmCVec, W, <.<. + , x. >., abs>.))))
18		opreq2 3969	. . . . . . 7 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> (if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpif(W e. NrmCVec, W, <.<. + , x. >., abs>.)))
19	18	fveq1d 3726	. . . . . 6 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> ((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T) = ((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpif(W e. NrmCVec, W, <.<. + , x. >., abs>.))` T))
20	19	eqeq1d 1483	. . . . 5 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> (((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T) = 0 <-> ((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpif(W e. NrmCVec, W, <.<. + , x. >., abs>.))` T) = 0))
21		opreq2 3969	. . . . . 6 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op if(W e. NrmCVec, W, <.<. + , x. >., abs>.)))
22	21	eqeq2d 1486	. . . . 5 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> (T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W) <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op if(W e. NrmCVec, W, <.<. + , x. >., abs>.))))
23	20, 22	bibi12d 629	. . . 4 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> ((((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T) = 0 <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W)) <-> (((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpif(W e. NrmCVec, W, <.<. + , x. >., abs>.))` T) = 0 <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op if(W e. NrmCVec, W, <.<. + , x. >., abs>.)))))
24	17, 23	imbi12d 626	. . 3 |- (W = if(W e. NrmCVec, W, <.<. + , x. >., abs>.) -> ((T e. (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp W) -> (((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpW)` T) = 0 <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op W))) <-> (T e. (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp if(W e. NrmCVec, W, <.<. + , x. >., abs>.)) -> (((if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpif(W e. NrmCVec, W, <.<. + , x. >., abs>.))` T) = 0 <-> T = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op if(W e. NrmCVec, W, <.<. + , x. >., abs>.))))))
25		eqid 1475	. . . 4 |- (if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpif(W e. NrmCVec, W, <.<. + , x. >., abs>.)) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.)normOpif(W e. NrmCVec, W, <.<. + , x. >., abs>.))
26		eqid 1475	. . . 4 |- (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op if(W e. NrmCVec, W, <.<. + , x. >., abs>.)) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) 0op if(W e. NrmCVec, W, <.<. + , x. >., abs>.))
27		eqid 1475	. . . 4 |- (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp if(W e. NrmCVec, W, <.<. + , x. >., abs>.)) = (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp if(W e. NrmCVec, W, <.<. + , x. >., abs>.))
28		elimnvu 8315	. . . 4 |- if(U e. NrmCVec, U, <.<. + , x. >., abs>.) e. NrmCVec
29		elimnvu 8315	. . . 4 |- if(W e. NrmCVec, W, <.<. + , x. >., abs>.) e. NrmCVec
30	25, 26, 27, 28, 29	nmlno0i 8454	. . 3 |- (T e. (if(U e. NrmCVec, U, <.<. + , x. >., abs>.) LnOp if(W e. NrmCVec, W, <.<. + , x. >., abs>.)) -> (((if(U e. NrmCVec, U,