Theorem nmofval 8425

Description: The operator norm function.

Hypotheses

Ref	Expression
nmofval.1	|- X = (Base` U)
nmofval.2	|- Y = (Base` W)
nmofval.3	|- L = (norm` U)
nmofval.4	|- M = (norm` W)
nmofval.6	|- N = (UnormOpW)

Assertion

Ref	Expression
nmofval	|- ((U e. NrmCVec /\ W e. NrmCVec) -> N = {<.t, y>. | (t:X-->Y /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < ))})

Distinct variable groups:   y,t,L   t,M,y   x,t,z,y,U   t,W,x,y,z   t,X,x,y,z   t,Y,x,y

Proof of Theorem nmofval

Step	Hyp	Ref	Expression
1		nmofval.2	. . . . . . . 8 |- Y = (Base` W)
2		fvex 3732	. . . . . . . 8 |- (Base` W) e. V
3	1, 2	eqeltr 1544	. . . . . . 7 |- Y e. V
4		nmofval.1	. . . . . . . 8 |- X = (Base` U)
5		fvex 3732	. . . . . . . 8 |- (Base` U) e. V
6	4, 5	eqeltr 1544	. . . . . . 7 |- X e. V
7	3, 6	elmap 4334	. . . . . 6 |- (t e. (Y ^m X) <-> t:X-->Y)
8	7	anbi1i 481	. . . . 5 |- ((t e. (Y ^m X) /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < )) <-> (t:X-->Y /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < )))
9	8	opabbii 2671	. . . 4 |- {<.t, y>. | (t e. (Y ^m X) /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < ))} = {<.t, y>. | (t:X-->Y /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < ))}
10		oprex 3983	. . . . 5 |- (Y ^m X) e. V
11	10	opabex2 3610	. . . 4 |- {<.t, y>. | (t e. (Y ^m X) /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < ))} e. V
12	9, 11	eqeltrr 1545	. . 3 |- {<.t, y>. | (t:X-->Y /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < ))} e. V
13		fveq2 3724	. . . . . . 7 |- (u = U -> (Base` u) = (Base` U))
14	13, 4	syl6eqr 1525	. . . . . 6 |- (u = U -> (Base` u) = X)
15		feq2 3621	. . . . . 6 |- ((Base` u) = X -> (t:(Base` u)-->(Base` w) <-> t:X-->(Base` w)))
16	14, 15	syl 10	. . . . 5 |- (u = U -> (t:(Base` u)-->(Base` w) <-> t:X-->(Base` w)))
17		fveq2 3724	. . . . . . . . . . . . 13 |- (u = U -> (norm` u) = (norm` U))
18		nmofval.3	. . . . . . . . . . . . 13 |- L = (norm` U)
19	17, 18	syl6eqr 1525	. . . . . . . . . . . 12 |- (u = U -> (norm` u) = L)
20	19	fveq1d 3726	. . . . . . . . . . 11 |- (u = U -> ((norm` u)` z) = (L` z))
21	20	breq1d 2629	. . . . . . . . . 10 |- (u = U -> (((norm` u)` z) <_ 1 <-> (L` z) <_ 1))
22	21	anbi1d 617	. . . . . . . . 9 |- (u = U -> ((((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z))) <-> ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))))
23	14, 22	rexeq12d 1795	. . . . . . . 8 |- (u = U -> (E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z))) <-> E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))))
24	23	abbidv 1577	. . . . . . 7 |- (u = U -> {x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))} = {x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))})
25		supeq1 4575	. . . . . . 7 |- ({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))} = {x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))} -> sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ) = sup({x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))
26	24, 25	syl 10	. . . . . 6 |- (u = U -> sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ) = sup({x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))
27	26	eqeq2d 1486	. . . . 5 |- (u = U -> (y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ) <-> y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )))
28	16, 27	anbi12d 628	. . . 4 |- (u = U -> ((t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )) <-> (t:X-->(Base` w) /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))))
29	28	opabbidv 2670	. . 3 |- (u = U -> {<.t, y>. | (t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))} = {<.t, y>. | (t:X-->(Base` w) /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})
30		fveq2 3724	. . . . . . 7 |- (w = W -> (Base` w) = (Base` W))
31	30, 1	syl6eqr 1525	. . . . . 6 |- (w = W -> (Base` w) = Y)
32		feq3 3622	. . . . . 6 |- ((Base` w) = Y -> (t:X-->(Base` w) <-> t:X-->Y))
33	31, 32	syl 10	. . . . 5 |- (w = W -> (t:X-->(Base` w) <-> t:X-->Y))
34		fveq2 3724	. . . . . . . . . . . . 13 |- (w = W -> (norm` w) = (norm` W))
35		nmofval.4	. . . . . . . . . . . . 13 |- M = (norm` W)
36	34, 35	syl6eqr 1525	. . . . . . . . . . . 12 |- (w = W -> (norm` w) = M)
37	36	fveq1d 3726	. . . . . . . . . . 11 |- (w = W -> ((norm` w)` (t` z)) = (M` (t` z)))
38	37	eqeq2d 1486	. . . . . . . . . 10 |- (w = W -> (x = ((norm` w)` (t` z)) <-> x = (M` (t` z))))
39	38	anbi2d 616	. . . . . . . . 9 |- (w = W -> (((L` z) <_ 1 /\ x = ((norm` w)` (t` z))) <-> ((L` z) <_ 1 /\ x = (M` (t` z)))))
40	39	rexbidv 1664	. . . . . . . 8 |- (w = W -> (E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z))) <-> E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))))
41	40	abbidv 1577	. . . . . . 7 |- (w = W -> {x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))} = {x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))})
42		supeq1 4575	. . . . . . 7 |- ({x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))} = {x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))} -> sup({x | E.z e. X ((L` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ) = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < ))
43	41, 42	syl 10	. . . . . 6 |- (w = W -> sup({x | E.z e. X