Theorem cnlnadjlem2 9996

Description: Lemma for cnlnadj 10004. G is a continuous linear functional.

Hypotheses

Ref	Expression
cnlnadjlem.1	|- T e. LinOp
cnlnadjlem.2	|- T e. ConOp
cnlnadjlem.3	|- G = {<.g, h>. | (g e. H~ /\ h = ((T` g) .ih y))}

Assertion

Ref	Expression
cnlnadjlem2	|- (y e. H~ -> (G e. LinFn /\ G e. ConFn))

Distinct variable group:   g,h,y,T

Proof of Theorem cnlnadjlem2

Step	Hyp	Ref	Expression
1		hiclt 8942	. . . . . . . 8 |- (((T` g) e. H~ /\ y e. H~) -> ((T` g) .ih y) e. CC)
2		cnlnadjlem.1	. . . . . . . . . 10 |- T e. LinOp
3	2	lnopf 9888	. . . . . . . . 9 |- T:H~-->H~
4	3	ffvelrni 3821	. . . . . . . 8 |- (g e. H~ -> (T` g) e. H~)
5	1, 4	sylan 450	. . . . . . 7 |- ((g e. H~ /\ y e. H~) -> ((T` g) .ih y) e. CC)
6	5	ancoms 438	. . . . . 6 |- ((y e. H~ /\ g e. H~) -> ((T` g) .ih y) e. CC)
7	6	r19.21aiva 1717	. . . . 5 |- (y e. H~ -> A.g e. H~ ((T` g) .ih y) e. CC)
8		cnlnadjlem.3	. . . . . 6 |- G = {<.g, h>. | (g e. H~ /\ h = ((T` g) .ih y))}
9	8	fopab2 3829	. . . . 5 |- (A.g e. H~ ((T` g) .ih y) e. CC <-> G:H~-->CC)
10	7, 9	sylib 198	. . . 4 |- (y e. H~ -> G:H~-->CC)
11	2	lnopadd 9890	. . . . . . . . . . . . . 14 |- (((x .h w) e. H~ /\ z e. H~) -> (T` ((x .h w) +h z)) = ((T` (x .h w)) +h (T` z)))
12	11	3adant3 801	. . . . . . . . . . . . 13 |- (((x .h w) e. H~ /\ z e. H~ /\ y e. H~) -> (T` ((x .h w) +h z)) = ((T` (x .h w)) +h (T` z)))
13	12	opreq1d 3981	. . . . . . . . . . . 12 |- (((x .h w) e. H~ /\ z e. H~ /\ y e. H~) -> ((T` ((x .h w) +h z)) .ih y) = (((T` (x .h w)) +h (T` z)) .ih y))
14		ax-his2 8945	. . . . . . . . . . . . 13 |- (((T` (x .h w)) e. H~ /\ (T` z) e. H~ /\ y e. H~) -> (((T` (x .h w)) +h (T` z)) .ih y) = (((T` (x .h w)) .ih y) + ((T` z) .ih y)))
15	3	ffvelrni 3821	. . . . . . . . . . . . 13 |- ((x .h w) e. H~ -> (T` (x .h w)) e. H~)
16	3	ffvelrni 3821	. . . . . . . . . . . . 13 |- (z e. H~ -> (T` z) e. H~)
17		id 59	. . . . . . . . . . . . 13 |- (y e. H~ -> y e. H~)
18	14, 15, 16, 17	syl3an 870	. . . . . . . . . . . 12 |- (((x .h w) e. H~ /\ z e. H~ /\ y e. H~) -> (((T` (x .h w)) +h (T` z)) .ih y) = (((T` (x .h w)) .ih y) + ((T` z) .ih y)))
19	13, 18	eqtrd 1510	. . . . . . . . . . 11 |- (((x .h w) e. H~ /\ z e. H~ /\ y e. H~) -> ((T` ((x .h w) +h z)) .ih y) = (((T` (x .h w)) .ih y) + ((T` z) .ih y)))
20	19	3comr 843	. . . . . . . . . 10 |- ((y e. H~ /\ (x .h w) e. H~ /\ z e. H~) -> ((T` ((x .h w) +h z)) .ih y) = (((T` (x .h w)) .ih y) + ((T` z) .ih y)))
21	20	3expa 835	. . . . . . . . 9 |- (((y e. H~ /\ (x .h w) e. H~) /\ z e. H~) -> ((T` ((x .h w) +h z)) .ih y) = (((T` (x .h w)) .ih y) + ((T` z) .ih y)))
22		hvmulclt 8878	. . . . . . . . 9 |- ((x e. CC /\ w e. H~) -> (x .h w) e. H~)
23	21, 22	sylanl2 463	. . . . . . . 8 |- (((y e. H~ /\ (x e. CC /\ w e. H~)) /\ z e. H~) -> ((T` ((x .h w) +h z)) .ih y) = (((T` (x .h w)) .ih y) + ((T` z) .ih y)))
24		hvaddclt 8877	. . . . . . . . . . 11 |- (((x .h w) e. H~ /\ z e. H~) -> ((x .h w) +h z) e. H~)
25	24, 22	sylan 450	. . . . . . . . . 10 |- (((x e. CC /\ w e. H~) /\ z e. H~) -> ((x .h w) +h z) e. H~)
26		cnlnadjlem.2	. . . . . . . . . . 11 |- T e. ConOp
27	2, 26, 8	cnlnadjlem1 9995	. . . . . . . . . 10 |- (((x .h w) +h z) e. H~ -> (G` ((x .h w) +h z)) = ((T` ((x .h w) +h z)) .ih y))
28	25, 27	syl 10	. . . . . . . . 9 |- (((x e. CC /\ w e. H~) /\ z e. H~) -> (G` ((x .h w) +h z)) = ((T` ((x .h w) +h z)) .ih y))
29	28	adantll 394	. . . . . . . 8 |- (((y e. H~ /\ (x e. CC /\ w e. H~)) /\ z e. H~) -> (G` ((x .h w) +h z)) = ((T` ((x .h w) +h z)) .ih y))
30		ax-his3 8946	. . . . . . . . . . . . 13 |- ((x e. CC /\ (T` w) e. H~ /\ y e. H~) -> ((x .h (T` w)) .ih y) = (x x. ((T` w) .ih y)))
31	3	ffvelrni 3821	. . . . . . . . . . . . 13 |- (w e. H~ -> (T` w) e. H~)
32	30, 31	syl3an2 862	. . . . . . . . . . . 12 |- ((x e. CC /\ w e. H~ /\ y e. H~) -> ((x .h (T` w)) .ih y) = (x x. ((T` w) .ih y)))
33	32	3comr 843	. . . . . . . . . . 11 |- ((y e. H~ /\ x e. CC /\ w e. H~) -> ((x .h (T` w)) .ih y) = (x x. ((T` w) .ih y)))
34	33	3expb 836	. . . . . . . . . 10 |- ((y e. H~ /\ (x e. CC /\ w e. H~)) -> ((x .h (T` w)) .ih y) = (x x. ((T` w) .ih y)))
35	2	lnopmul 9891	. . . . . . . . . . . 12 |- ((x e. CC /\ w e. H~) -> (T` (x .h w)) = (x .h (T` w)))
36	35	opreq1d 3981	. . . . . . . . . . 11 |- ((x e. CC /\ w e. H~) -> ((T` (x .h w)) .ih y) = ((x .h (T` w)) .ih y))
37	36	adantl 390	. . . . . . . . . 10 |- ((y e. H~ /\ (x e. CC /\ w e. H~)) -> ((T` (x .h w)) .ih y) = ((x .h (T` w)) .ih y))
38	2, 26, 8	cnlnadjlem1 9995	. . . . . . . . . . . 12 |- (w e. H~ -> (G` w) = ((T` w) .ih y))
39	38	opreq2d 3982	. . . . . . . . . . 11 |- (w e. H~ -> (x x. (G` w)) = (x x. ((T` w) .ih y)))
40	39	ad2antll 409	. . . . . . . . . 10 |- ((y e. H~ /\ (x e. CC /\ w e. H~)) -> (x x. (G` w)) = (x x. ((T` w) .ih y)))
41	34, 37, 40	3eqtr4rd 1521	. . . . . . . . 9 |- ((y e. H~ /\ (x e. CC /\ w e. H~)) -> (x x. (G` w)) = ((T` (x .h w)) .ih y))
42	2, 26, 8	cnlnadjlem1 9995	. . . . . . . . 9 |- (z e. H~ -> (G` z) = ((T` z) .ih y))
43	41, 42	opreqan12d 3985	. . . . . . . 8 |- (((y e. H~ /\ (x e. CC /\ w e. H~)) /\ z e. H~) -> ((x x. (G` w)) + (G` z)) = (((T` (x .h w)) .ih y) + ((T` z) .ih y)))
44	23, 29, 43	3eqtr4d 1520	. . . . . . 7 |- (((y e. H~ /\ (x e. CC /\ w e. H~)) /\ z e. H~) -> (G` ((x .h w) +h z)) = ((x x. (G` w)) + (G` z)))
45	44	r19.21aiva 1717	. . . . . 6 |- ((y e. H~ /\ (x e. CC /\ w e. H~)) -> A.z e. H~ (G` ((x .h w) +h z)) = ((x x. (G` w)) + (G` z)))
46	45	ex 373	. . . . 5 |- (y e. H~ -> ((x e. CC /\ w e. H~) -> A.z e. H~ (G` ((x .h w) +h z)) = ((x x. (G` w)) + (G` z))))
47	46	r19.21aivv 1723	. . . 4 |- (y e. H~ -> A.x e. CC A.w e. H~ A.z e. H~ (G` ((x .h w) +h z)) = ((x x. (G` w)) + (G` z)))
48	10, 47	jca 288	. . 3 |- (y e. H~ -> (G:H~-->CC /\ A.x e. CC A.w e. H~ A.z e. H~ (G` ((x .h w) +h z)) = ((x x. (G` w)) + (G` z))))
49		ellnfnt 9805	. . 3 |- (G e. LinFn <-> (G:H~-->CC /\ A.x e. CC A.w e. H~ A.z e. H~ (G` ((x .h w) +h z)) = ((x x. (G` w)) + (G` z))))
50	48, 49	sylibr 200	. 2 |- (y e. H~ -> G e. LinFn)
51		opreq1 3974	. . . . . . 7 |- (x = ((normop` T) x. (normh` y)) -> (x x. (normh` z)) = (((normop` T) x. (normh` y)) x. (normh` z)))
52	51	breq2d 2635	. . . . . 6 |- (x = ((normop` T) x. (normh` y)) -> ((abs` (G` z)) <_ (x x. (normh` z))