Theorem cnlnadjlem6 10000

Description: Lemma for cnlnadj 10004. F is linear.

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))}
cnlnadjlem.4	|- B = U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)}
cnlnadjlem.5	|- F = {<.y, u>. | (y e. H~ /\ u = B)}

Assertion

Ref	Expression
cnlnadjlem6	|- F e. LinOp

Distinct variable groups:   g,h,u,v,w,y   u,B   w,F   v,G,w   T,g,h,u,v,w,y

Proof of Theorem cnlnadjlem6

Step	Hyp	Ref	Expression
1		ellnopt 9779	. 2 |- (F e. LinOp <-> (F:H~-->H~ /\ A.x e. CC A.f e. H~ A.z e. H~ (F` ((x .h f) +h z)) = ((x .h (F` f)) +h (F` z))))
2		cnlnadjlem.5	. . 3 |- F = {<.y, u>. | (y e. H~ /\ u = B)}
3		cnlnadjlem.1	. . . 4 |- T e. LinOp
4		cnlnadjlem.2	. . . 4 |- T e. ConOp
5		cnlnadjlem.3	. . . 4 |- G = {<.g, h>. | (g e. H~ /\ h = ((T` g) .ih y))}
6		cnlnadjlem.4	. . . 4 |- B = U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)}
7	3, 4, 5, 6, 2	cnlnadjlem3 9997	. . 3 |- (y e. H~ -> B e. H~)
8	2, 7	fopab 3833	. 2 |- F:H~-->H~
9		his7t 8951	. . . . . . . 8 |- (((T` t) e. H~ /\ (x .h f) e. H~ /\ z e. H~) -> ((T` t) .ih ((x .h f) +h z)) = (((T` t) .ih (x .h f)) + ((T` t) .ih z)))
10	3	lnopf 9888	. . . . . . . . . 10 |- T:H~-->H~
11	10	ffvelrni 3821	. . . . . . . . 9 |- (t e. H~ -> (T` t) e. H~)
12	11	adantl 390	. . . . . . . 8 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (T` t) e. H~)
13		hvmulclt 8878	. . . . . . . . 9 |- ((x e. CC /\ f e. H~) -> (x .h f) e. H~)
14	13	ad2antrr 406	. . . . . . . 8 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (x .h f) e. H~)
15		simplr 415	. . . . . . . 8 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> z e. H~)
16	9, 12, 14, 15	syl3anc 860	. . . . . . 7 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> ((T` t) .ih ((x .h f) +h z)) = (((T` t) .ih (x .h f)) + ((T` t) .ih z)))
17	3, 4, 5, 6, 2	cnlnadjlem5 9999	. . . . . . . 8 |- ((((x .h f) +h z) e. H~ /\ t e. H~) -> ((T` t) .ih ((x .h f) +h z)) = (t .ih (F` ((x .h f) +h z))))
18		hvaddclt 8877	. . . . . . . . 9 |- (((x .h f) e. H~ /\ z e. H~) -> ((x .h f) +h z) e. H~)
19	18, 13	sylan 450	. . . . . . . 8 |- (((x e. CC /\ f e. H~) /\ z e. H~) -> ((x .h f) +h z) e. H~)
20	17, 19	sylan 450	. . . . . . 7 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> ((T` t) .ih ((x .h f) +h z)) = (t .ih (F` ((x .h f) +h z))))
21	3, 4, 5, 6, 2	cnlnadjlem5 9999	. . . . . . . . . . . . 13 |- ((f e. H~ /\ t e. H~) -> ((T` t) .ih f) = (t .ih (F` f)))
22	21	adantll 394	. . . . . . . . . . . 12 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> ((T` t) .ih f) = (t .ih (F` f)))
23	22	opreq2d 3982	. . . . . . . . . . 11 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> ((*` x) x. ((T` t) .ih f)) = ((*` x) x. (t .ih (F` f))))
24		his5t 8948	. . . . . . . . . . . 12 |- ((x e. CC /\ (T` t) e. H~ /\ f e. H~) -> ((T` t) .ih (x .h f)) = ((*` x) x. ((T` t) .ih f)))
25		simpll 414	. . . . . . . . . . . 12 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> x e. CC)
26	11	adantl 390	. . . . . . . . . . . 12 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> (T` t) e. H~)
27		simplr 415	. . . . . . . . . . . 12 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> f e. H~)
28	24, 25, 26, 27	syl3anc 860	. . . . . . . . . . 11 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> ((T` t) .ih (x .h f)) = ((*` x) x. ((T` t) .ih f)))
29		his5t 8948	. . . . . . . . . . . 12 |- ((x e. CC /\ t e. H~ /\ (F` f) e. H~) -> (t .ih (x .h (F` f))) = ((*` x) x. (t .ih (F` f))))
30		pm3.27 323	. . . . . . . . . . . 12 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> t e. H~)
31	3, 4, 5, 6, 2	cnlnadjlem4 9998	. . . . . . . . . . . . 13 |- (f e. H~ -> (F` f) e. H~)
32	31	ad2antlr 407	. . . . . . . . . . . 12 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> (F` f) e. H~)
33	29, 25, 30, 32	syl3anc 860	. . . . . . . . . . 11 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> (t .ih (x .h (F` f))) = ((*` x) x. (t .ih (F` f))))
34	23, 28, 33	3eqtr4d 1520	. . . . . . . . . 10 |- (((x e. CC /\ f e. H~) /\ t e. H~) -> ((T` t) .ih (x .h f)) = (t .ih (x .h (F` f))))
35	34	adantlr 395	. . . . . . . . 9 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> ((T` t) .ih (x .h f)) = (t .ih (x .h (F` f))))
36	3, 4, 5, 6, 2	cnlnadjlem5 9999	. . . . . . . . . 10 |- ((z e. H~ /\ t e. H~) -> ((T` t) .ih z) = (t .ih (F` z)))
37	36	adantll 394	. . . . . . . . 9 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> ((T` t) .ih z) = (t .ih (F` z)))
38	35, 37	opreq12d 3984	. . . . . . . 8 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (((T` t) .ih (x .h f)) + ((T` t) .ih z)) = ((t .ih (x .h (F` f))) + (t .ih (F` z))))
39		his7t 8951	. . . . . . . . 9 |- ((t e. H~ /\ (x .h (F` f)) e. H~ /\ (F` z) e. H~) -> (t .ih ((x .h (F` f)) +h (F` z))) = ((t .ih (x .h (F` f))) + (t .ih (F` z))))
40		pm3.27 323	. . . . . . . . 9 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> t e. H~)
41		hvmulclt 8878	. . . . . . . . . . 11 |- ((x e. CC /\ (F` f) e. H~) -> (x .h (F` f)) e. H~)
42	41, 31	sylan2 453	. . . . . . . . . 10 |- ((x e. CC /\ f e. H~) -> (x .h (F` f)) e. H~)
43	42	ad2antrr 406	. . . . . . . . 9 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (x .h (F` f)) e. H~)
44	3, 4, 5, 6, 2	cnlnadjlem4 9998	. . . . . . . . . 10 |- (z e. H~ -> (F` z) e. H~)
45	44	ad2antlr 407	. . . . . . . . 9 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (F` z) e. H~)
46	39, 40, 43, 45	syl3anc 860	. . . . . . . 8 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (t .ih ((x .h (F` f)) +h (F` z))) = ((t .ih (x .h (F` f))) + (t .ih (F` z))))
47	38, 46	eqtr4d 1513	. . . . . . 7 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (((T` t) .ih (x .h f)) + ((T` t) .ih z)) = (t .ih ((x .h (F` f)) +h (F` z))))
48	16, 20, 47	3eqtr3d 1518	. . . . . 6 |- ((((x e. CC /\ f e. H~) /\ z e. H~) /\ t e. H~) -> (t .ih (F` ((x .h f) +h z))) = (t .ih ((x .h (F` f)) +h (F` z))))
49	48	r19.21aiva 1717	. . . . 5 |- (((x e. CC /\ f e. H~) /\ z e. H~) -> A.t e. H~ (t .ih (F` ((x .h f) +h z))) = (t .ih ((x .h (F` f)) +h (F` z))))
50		hial2eq2t 8968	. . . . . 6 |- (((F` ((x .h f) +h z)) e. H~ /\ ((x .h (F` f)) +h (F` z)) e. H~) -> (A.t e. H~ (t .ih (F` ((x .h f) +h z))) = (t .ih ((x .h (F` f)) +h (F` z))) <-> (F` ((x .h f) +h z)) = ((x .h (F` f)) +h (F` z))))
51	3, 4, 5, 6, 2	cnlnadjlem4 9998	. . . . . . 7 |- (((x .h f) +h z) e.