Theorem adjlnopt 10014

Description: The adjoint of an operator is linear. Proposition 1 of [AkhiezerGlazman] p. 80.

Assertion

Ref	Expression
adjlnopt	|- (T e. dom adjh -> (adjh` T) e. LinOp)

Proof of Theorem adjlnopt

Step	Hyp	Ref	Expression
1		dmadjrnt 9816	. . . 4 |- (T e. dom adjh -> (adjh` T) e. dom adjh)
2		dmadjopt 9815	. . . 4 |- ((adjh` T) e. dom adjh -> (adjh` T):H~-->H~)
3	1, 2	syl 10	. . 3 |- (T e. dom adjh -> (adjh` T):H~-->H~)
4		his7t 8951	. . . . . . . . . . . 12 |- (((T` w) e. H~ /\ (x .h y) e. H~ /\ z e. H~) -> ((T` w) .ih ((x .h y) +h z)) = (((T` w) .ih (x .h y)) + ((T` w) .ih z)))
5		ffvelrn 3820	. . . . . . . . . . . . . 14 |- ((T:H~-->H~ /\ w e. H~) -> (T` w) e. H~)
6		dmadjopt 9815	. . . . . . . . . . . . . 14 |- (T e. dom adjh -> T:H~-->H~)
7	5, 6	sylan 450	. . . . . . . . . . . . 13 |- ((T e. dom adjh /\ w e. H~) -> (T` w) e. H~)
8	7	3adant3 801	. . . . . . . . . . . 12 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> (T` w) e. H~)
9		hvmulclt 8878	. . . . . . . . . . . . . 14 |- ((x e. CC /\ y e. H~) -> (x .h y) e. H~)
10	9	adantr 391	. . . . . . . . . . . . 13 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> (x .h y) e. H~)
11	10	3ad2ant3 804	. . . . . . . . . . . 12 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> (x .h y) e. H~)
12		pm3.27 323	. . . . . . . . . . . . 13 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> z e. H~)
13	12	3ad2ant3 804	. . . . . . . . . . . 12 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> z e. H~)
14	4, 8, 11, 13	syl3anc 860	. . . . . . . . . . 11 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> ((T` w) .ih ((x .h y) +h z)) = (((T` w) .ih (x .h y)) + ((T` w) .ih z)))
15		adj2t 9853	. . . . . . . . . . . 12 |- ((T e. dom adjh /\ w e. H~ /\ ((x .h y) +h z) e. H~) -> ((T` w) .ih ((x .h y) +h z)) = (w .ih ((adjh` T)` ((x .h y) +h z))))
16		hvaddclt 8877	. . . . . . . . . . . . 13 |- (((x .h y) e. H~ /\ z e. H~) -> ((x .h y) +h z) e. H~)
17	16, 9	sylan 450	. . . . . . . . . . . 12 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((x .h y) +h z) e. H~)
18	15, 17	syl3an3 863	. . . . . . . . . . 11 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> ((T` w) .ih ((x .h y) +h z)) = (w .ih ((adjh` T)` ((x .h y) +h z))))
19		adj2t 9853	. . . . . . . . . . . . . . . . 17 |- ((T e. dom adjh /\ w e. H~ /\ y e. H~) -> ((T` w) .ih y) = (w .ih ((adjh` T)` y)))
20	19	3adant3l 858	. . . . . . . . . . . . . . . 16 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> ((T` w) .ih y) = (w .ih ((adjh` T)` y)))
21	20	opreq2d 3982	. . . . . . . . . . . . . . 15 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> ((*` x) x. ((T` w) .ih y)) = ((*` x) x. (w .ih ((adjh` T)` y))))
22		his5t 8948	. . . . . . . . . . . . . . . 16 |- ((x e. CC /\ (T` w) e. H~ /\ y e. H~) -> ((T` w) .ih (x .h y)) = ((*` x) x. ((T` w) .ih y)))
23		pm3.26 319	. . . . . . . . . . . . . . . . 17 |- ((x e. CC /\ y e. H~) -> x e. CC)
24	23	3ad2ant3 804	. . . . . . . . . . . . . . . 16 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> x e. CC)
25	7	3adant3 801	. . . . . . . . . . . . . . . 16 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> (T` w) e. H~)
26		pm3.27 323	. . . . . . . . . . . . . . . . 17 |- ((x e. CC /\ y e. H~) -> y e. H~)
27	26	3ad2ant3 804	. . . . . . . . . . . . . . . 16 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> y e. H~)
28	22, 24, 25, 27	syl3anc 860	. . . . . . . . . . . . . . 15 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> ((T` w) .ih (x .h y)) = ((*` x) x. ((T` w) .ih y)))
29		his5t 8948	. . . . . . . . . . . . . . . 16 |- ((x e. CC /\ w e. H~ /\ ((adjh` T)` y) e. H~) -> (w .ih (x .h ((adjh` T)` y))) = ((*` x) x. (w .ih ((adjh` T)` y))))
30		3simp2 791	. . . . . . . . . . . . . . . 16 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> w e. H~)
31		adjclt 9851	. . . . . . . . . . . . . . . . . 18 |- ((T e. dom adjh /\ y e. H~) -> ((adjh` T)` y) e. H~)
32	31	adantrl 396	. . . . . . . . . . . . . . . . 17 |- ((T e. dom adjh /\ (x e. CC /\ y e. H~)) -> ((adjh` T)` y) e. H~)
33	32	3adant2 800	. . . . . . . . . . . . . . . 16 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> ((adjh` T)` y) e. H~)
34	29, 24, 30, 33	syl3anc 860	. . . . . . . . . . . . . . 15 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> (w .ih (x .h ((adjh` T)` y))) = ((*` x) x. (w .ih ((adjh` T)` y))))
35	21, 28, 34	3eqtr4d 1520	. . . . . . . . . . . . . 14 |- ((T e. dom adjh /\ w e. H~ /\ (x e. CC /\ y e. H~)) -> ((T` w) .ih (x .h y)) = (w .ih (x .h ((adjh` T)` y))))
36	35	3adant3r 859	. . . . . . . . . . . . 13 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> ((T` w) .ih (x .h y)) = (w .ih (x .h ((adjh` T)` y))))
37		adj2t 9853	. . . . . . . . . . . . . 14 |- ((T e. dom adjh /\ w e. H~ /\ z e. H~) -> ((T` w) .ih z) = (w .ih ((adjh` T)` z)))
38	37	3adant3l 858	. . . . . . . . . . . . 13 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> ((T` w) .ih z) = (w .ih ((adjh` T)` z)))
39	36, 38	opreq12d 3984	. . . . . . . . . . . 12 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> (((T` w) .ih (x .h y)) + ((T` w) .ih z)) = ((w .ih (x .h ((adjh` T)` y))) + (w .ih ((adjh` T)` z))))
40		his7t 8951	. . . . . . . . . . . . 13 |- ((w e. H~ /\ (x .h ((adjh` T)` y)) e. H~ /\ ((adjh` T)` z) e. H~) -> (w .ih ((x .h ((adjh` T)` y)) +h ((adjh` T)` z))) = ((w .ih (x .h ((adjh` T)` y))) + (w .ih ((adjh` T)` z))))
41		3simp2 791	. . . . . . . . . . . . 13 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> w e. H~)
42		hvmulclt 8878	. . . . . . . . . . . . . . . . 17 |- ((x e. CC /\ ((adjh` T)` y) e. H~) -> (x .h ((adjh` T)` y)) e. H~)
43	42, 31	sylan2 453	. . . . . . . . . . . . . . . 16 |- ((x e. CC /\ (T e. dom adjh /\ y e. H~)) -> (x .h ((adjh` T)` y)) e. H~)
44	43	an1s 488	. . . . . . . . . . . . . . 15 |- ((T e. dom adjh /\ (x e. CC /\ y e. H~)) -> (x .h ((adjh` T)` y)) e. H~)
45	44	adantrr 397	. . . . . . . . . . . . . 14 |- ((T e. dom adjh /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> (x .h ((adjh` T)` y)) e. H~)
46	45	3adant2 800	. . . . . . . . . . . . 13 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> (x .h ((adjh` T)` y)) e. H~)
47		adjclt 9851	. . . . . . . . . . . . . . 15 |- ((T e. dom adjh /\ z e. H~) -> ((adjh` T)` z) e. H~)
48	47	adantrl 396	. . . . . . . . . . . . . 14 |- ((T e. dom adjh /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> ((adjh` T)` z) e. H~)
49	48	3adant2 800	. . . . . . . . . . . . 13 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> ((adjh` T)` z) e. H~)
50	40, 41, 46, 49	syl3anc 860	. . . . . . . . . . . 12 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> (w .ih ((x .h ((adjh` T)` y)) +h ((adjh` T)` z))) = ((w .ih (x .h ((adjh` T)` y))) + (w .ih ((adjh` T)` z))))
51	39, 50	eqtr4d 1513	. . . . . . . . . . 11 |- ((T e. dom adjh /\ w e. H~ /\ ((x e. CC /\ y e. H~) /\ z e. H~)) -> (