Theorem lnoval 8413

Description: The set of linear operators between two normed complex vector spaces.

Hypotheses

Ref	Expression
lnoval.1	|- X = (Base` U)
lnoval.2	|- Y = (Base` W)
lnoval.3	|- G = (+v` U)
lnoval.4	|- H = (+v` W)
lnoval.5	|- R = (.s` U)
lnoval.6	|- S = (.s` W)
lnoval.7	|- L = (U LnOp W)

Assertion

Ref	Expression
lnoval	|- ((U e. NrmCVec /\ W e. NrmCVec) -> L = {t | (t:X-->Y /\ A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)H(yS(t` z))))})

Distinct variable groups:   t,G   t,H   t,R   t,S   x,t,y,z,U   t,W,x,y,z   t,X,x,y,z   t,Y

Proof of Theorem lnoval

Step	Hyp	Ref	Expression
1		lnoval.1	. . . . 5 |- X = (Base` U)
2		fvex 3732	. . . . 5 |- (Base` U) e. V
3	1, 2	eqeltr 1544	. . . 4 |- X e. V
4		lnoval.2	. . . . 5 |- Y = (Base` W)
5		fvex 3732	. . . . 5 |- (Base` W) e. V
6	4, 5	eqeltr 1544	. . . 4 |- Y e. V
7		eqid 1475	. . . 4 |- {t | (t:X-->Y /\ A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)H(yS(t` z))))} = {t | (t:X-->Y /\ A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)H(yS(t` z))))}
8	3, 6, 7	fabex 3654	. . 3 |- {t | (t:X-->Y /\ A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)H(yS(t` z))))} e. V
9		fveq2 3724	. . . . . . 7 |- (u = U -> (Base` u) = (Base` U))
10	9, 1	syl6eqr 1525	. . . . . 6 |- (u = U -> (Base` u) = X)
11		feq2 3621	. . . . . 6 |- ((Base` u) = X -> (t:(Base` u)-->(Base` w) <-> t:X-->(Base` w)))
12	10, 11	syl 10	. . . . 5 |- (u = U -> (t:(Base` u)-->(Base` w) <-> t:X-->(Base` w)))
13		fveq2 3724	. . . . . . . . . . . . . 14 |- (u = U -> (.s` u) = (.s` U))
14		lnoval.5	. . . . . . . . . . . . . 14 |- R = (.s` U)
15	13, 14	syl6eqr 1525	. . . . . . . . . . . . 13 |- (u = U -> (.s` u) = R)
16	15	opreqd 3977	. . . . . . . . . . . 12 |- (u = U -> (y(.s` u)z) = (yRz))
17	16	opreq2d 3976	. . . . . . . . . . 11 |- (u = U -> (x(+v` u)(y(.s` u)z)) = (x(+v` u)(yRz)))
18		fveq2 3724	. . . . . . . . . . . . 13 |- (u = U -> (+v` u) = (+v` U))
19		lnoval.3	. . . . . . . . . . . . 13 |- G = (+v` U)
20	18, 19	syl6eqr 1525	. . . . . . . . . . . 12 |- (u = U -> (+v` u) = G)
21	20	opreqd 3977	. . . . . . . . . . 11 |- (u = U -> (x(+v` u)(yRz)) = (xG(yRz)))
22	17, 21	eqtrd 1507	. . . . . . . . . 10 |- (u = U -> (x(+v` u)(y(.s` u)z)) = (xG(yRz)))
23	22	fveq2d 3728	. . . . . . . . 9 |- (u = U -> (t` (x(+v` u)(y(.s` u)z))) = (t` (xG(yRz))))
24	23	eqeq1d 1483	. . . . . . . 8 |- (u = U -> ((t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))) <-> (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z)))))
25	10, 24	raleq12d 1794	. . . . . . 7 |- (u = U -> (A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))) <-> A.z e. X (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z)))))
26	25	ralbidv 1663	. . . . . 6 |- (u = U -> (A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))) <-> A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z)))))
27	10, 26	raleq12d 1794	. . . . 5 |- (u = U -> (A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))) <-> A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z)))))
28	12, 27	anbi12d 628	. . . 4 |- (u = U -> ((t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z)))) <-> (t:X-->(Base` w) /\ A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z))))))
29	28	abbidv 1577	. . 3 |- (u = U -> {t | (t:(Base` u)-->(Base` w) /\ A.x e. (Base` u)A.y e. CC A.z e. (Base` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))} = {t | (t:X-->(Base` w) /\ A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})
30		fveq2 3724	. . . . . . 7 |- (w = W -> (Base` w) = (Base` W))
31	30, 4	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	. . . . . . . . . . . 12 |- (w = W -> (.s` w) = (.s` W))
35		lnoval.6	. . . . . . . . . . . 12 |- S = (.s` W)
36	34, 35	syl6eqr 1525	. . . . . . . . . . 11 |- (w = W -> (.s` w) = S)
37	36	opreqd 3977	. . . . . . . . . 10 |- (w = W -> (y(.s` w)(t` z)) = (yS(t` z)))
38	37	opreq2d 3976	. . . . . . . . 9 |- (w = W -> ((t` x)(+v` w)(y(.s` w)(t` z))) = ((t` x)(+v` w)(yS(t` z))))
39		fveq2 3724	. . . . . . . . . . 11 |- (w = W -> (+v` w) = (+v` W))
40		lnoval.4	. . . . . . . . . . 11 |- H = (+v` W)
41	39, 40	syl6eqr 1525	. . . . . . . . . 10 |- (w = W -> (+v` w) = H)
42	41	opreqd 3977	. . . . . . . . 9 |- (w = W -> ((t` x)(+v` w)(yS(t` z))) = ((t` x)H(yS(t` z))))
43	38, 42	eqtrd 1507	. . . . . . . 8 |- (w = W -> ((t` x)(+v` w)(y(.s` w)(t` z))) = ((t` x)H(yS(t` z))))
44	43	eqeq2d 1486	. . . . . . 7 |- (w = W -> ((t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z))) <-> (t` (xG(yRz))) = ((t` x)H(yS(t` z)))))
45	44	ralbidv 1663	. . . . . 6 |- (w = W -> (A.z e. X (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z))) <-> A.z e. X (t` (xG(yRz))) = ((t` x)H(yS(t` z)))))
46	45	2ralbidv 1680	. . . . 5 |- (w = W -> (A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)(+v` w)(y(.s` w)(t` z))) <-> A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)H(yS(t` z)))))
47	33, 46	anbi12d 628	. . . 4 |- (w = W -> ((t:X-->(Base` w) /\ A.x e. X A.y e. CC A.z e. X (t` (xG