Theorem adjaddt 9940

Description: The adjoint of the sum of two operators. Theorem 3.11(iii) of [Beran] p. 106.

Assertion

Ref	Expression
adjaddt	|- ((S e. dom adjh /\ T e. dom adjh) -> (adjh` (S +op T)) = ((adjh` S) +op (adjh` T)))

Proof of Theorem adjaddt

Step	Hyp	Ref	Expression
1		adjeqt 9775	. 2 |- (((S +op T):H~-->H~ /\ ((adjh` S) +op (adjh` T)):H~-->H~ /\ A.x e. H~ A.y e. H~ (((S +op T)` x) .ih y) = (x .ih (((adjh` S) +op (adjh` T))` y))) -> (adjh` (S +op T)) = ((adjh` S) +op (adjh` T)))
2		hoaddclt 9601	. . 3 |- ((S:H~-->H~ /\ T:H~-->H~) -> (S +op T):H~-->H~)
3		dmadjopt 9737	. . 3 |- (S e. dom adjh -> S:H~-->H~)
4		dmadjopt 9737	. . 3 |- (T e. dom adjh -> T:H~-->H~)
5	2, 3, 4	syl2an 454	. 2 |- ((S e. dom adjh /\ T e. dom adjh) -> (S +op T):H~-->H~)
6		hoaddclt 9601	. . 3 |- (((adjh` S):H~-->H~ /\ (adjh` T):H~-->H~) -> ((adjh` S) +op (adjh` T)):H~-->H~)
7		dmadjrnt 9738	. . . 4 |- (S e. dom adjh -> (adjh` S) e. dom adjh)
8		dmadjopt 9737	. . . 4 |- ((adjh` S) e. dom adjh -> (adjh` S):H~-->H~)
9	7, 8	syl 10	. . 3 |- (S e. dom adjh -> (adjh` S):H~-->H~)
10		dmadjrnt 9738	. . . 4 |- (T e. dom adjh -> (adjh` T) e. dom adjh)
11		dmadjopt 9737	. . . 4 |- ((adjh` T) e. dom adjh -> (adjh` T):H~-->H~)
12	10, 11	syl 10	. . 3 |- (T e. dom adjh -> (adjh` T):H~-->H~)
13	6, 9, 12	syl2an 454	. 2 |- ((S e. dom adjh /\ T e. dom adjh) -> ((adjh` S) +op (adjh` T)):H~-->H~)
14		ax-his2 8871	. . . . . . . 8 |- (((S` x) e. H~ /\ (T` x) e. H~ /\ y e. H~) -> (((S` x) +h (T` x)) .ih y) = (((S` x) .ih y) + ((T` x) .ih y)))
15		ffvelrn 3799	. . . . . . . . . 10 |- ((S:H~-->H~ /\ x e. H~) -> (S` x) e. H~)
16	15, 3	sylan 448	. . . . . . . . 9 |- ((S e. dom adjh /\ x e. H~) -> (S` x) e. H~)
17	16	ad2ant2r 409	. . . . . . . 8 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (S` x) e. H~)
18		ffvelrn 3799	. . . . . . . . . 10 |- ((T:H~-->H~ /\ x e. H~) -> (T` x) e. H~)
19	18, 4	sylan 448	. . . . . . . . 9 |- ((T e. dom adjh /\ x e. H~) -> (T` x) e. H~)
20	19	ad2ant2lr 410	. . . . . . . 8 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (T` x) e. H~)
21		simprr 415	. . . . . . . 8 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> y e. H~)
22	14, 17, 20, 21	syl3anc 856	. . . . . . 7 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (((S` x) +h (T` x)) .ih y) = (((S` x) .ih y) + ((T` x) .ih y)))
23		adj2t 9774	. . . . . . . . . 10 |- ((S e. dom adjh /\ x e. H~ /\ y e. H~) -> ((S` x) .ih y) = (x .ih ((adjh` S)` y)))
24	23	3expb 832	. . . . . . . . 9 |- ((S e. dom adjh /\ (x e. H~ /\ y e. H~)) -> ((S` x) .ih y) = (x .ih ((adjh` S)` y)))
25	24	adantlr 393	. . . . . . . 8 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> ((S` x) .ih y) = (x .ih ((adjh` S)` y)))
26		adj2t 9774	. . . . . . . . . 10 |- ((T e. dom adjh /\ x e. H~ /\ y e. H~) -> ((T` x) .ih y) = (x .ih ((adjh` T)` y)))
27	26	3expb 832	. . . . . . . . 9 |- ((T e. dom adjh /\ (x e. H~ /\ y e. H~)) -> ((T` x) .ih y) = (x .ih ((adjh` T)` y)))
28	27	adantll 392	. . . . . . . 8 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> ((T` x) .ih y) = (x .ih ((adjh` T)` y)))
29	25, 28	opreq12d 3963	. . . . . . 7 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (((S` x) .ih y) + ((T` x) .ih y)) = ((x .ih ((adjh` S)` y)) + (x .ih ((adjh` T)` y))))
30	22, 29	eqtrd 1499	. . . . . 6 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (((S` x) +h (T` x)) .ih y) = ((x .ih ((adjh` S)` y)) + (x .ih ((adjh` T)` y))))
31		hosvaltOLD 9434	. . . . . . . . 9 |- (((S:H~-->H~ /\ T:H~-->H~) /\ x e. H~) -> ((S +op T)` x) = ((S` x) +h (T` x)))
32	3, 4	anim12i 333	. . . . . . . . 9 |- ((S e. dom adjh /\ T e. dom adjh) -> (S:H~-->H~ /\ T:H~-->H~))
33	31, 32	sylan 448	. . . . . . . 8 |- (((S e. dom adjh /\ T e. dom adjh) /\ x e. H~) -> ((S +op T)` x) = ((S` x) +h (T` x)))
34	33	adantrr 395	. . . . . . 7 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> ((S +op T)` x) = ((S` x) +h (T` x)))
35	34	opreq1d 3960	. . . . . 6 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (((S +op T)` x) .ih y) = (((S` x) +h (T` x)) .ih y))
36		his7t 8877	. . . . . . 7 |- ((x e. H~ /\ ((adjh` S)` y) e. H~ /\ ((adjh` T)` y) e. H~) -> (x .ih (((adjh` S)` y) +h ((adjh` T)` y))) = ((x .ih ((adjh` S)` y)) + (x .ih ((adjh` T)` y))))
37		simprl 414	. . . . . . 7 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> x e. H~)
38		adjclt 9772	. . . . . . . 8 |- ((S e. dom adjh /\ y e. H~) -> ((adjh` S)` y) e. H~)
39	38	ad2ant2rl 411	. . . . . . 7 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> ((adjh` S)` y) e. H~)
40		adjclt 9772	. . . . . . . 8 |- ((T e. dom adjh /\ y e. H~) -> ((adjh` T)` y) e. H~)
41	40	ad2ant2l 408	. . . . . . 7 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> ((adjh` T)` y) e. H~)
42	36, 37, 39, 41	syl3anc 856	. . . . . 6 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (x .ih (((adjh` S)` y) +h ((adjh` T)` y))) = ((x .ih ((adjh` S)` y)) + (x .ih ((adjh` T)` y))))
43	30, 35, 42	3eqtr4d 1509	. . . . 5 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (((S +op T)` x) .ih y) = (x .ih (((adjh` S)` y) +h ((adjh` T)` y))))
44		hosvaltOLD 9434	. . . . . . . 8 |- ((((adjh` S):H~-->H~ /\ (adjh` T):H~-->H~) /\ y e. H~) -> (((adjh` S) +op (adjh` T))` y) = (((adjh` S)` y) +h ((adjh` T)` y)))
45	9, 12	anim12i 333	. . . . . . . 8 |- ((S e. dom adjh /\ T e. dom adjh) -> ((adjh` S):H~-->H~ /\ (adjh` T):H~-->H~))
46	44, 45	sylan 448	. . . . . . 7 |- (((S e. dom adjh /\ T e. dom adjh) /\ y e. H~) -> (((adjh` S) +op (adjh` T))` y) = (((adjh` S)` y) +h ((adjh` T)` y)))
47	46	adantrl 394	. . . . . 6 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (((adjh` S) +op (adjh` T))` y) = (((adjh` S)` y) +h ((adjh` T)` y)))
48	47	opreq2d 3961	. . . . 5 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (x .ih (((adjh` S) +op (adjh` T))` y)) = (x .ih (((adjh` S)` y) +h ((adjh` T)` y))))
49	43, 48	eqtr4d 1502	. . . 4 |- (((S e. dom adjh /\ T e. dom adjh) /\ (x e. H~ /\ y e. H~)) -> (((S +op T)` x) .ih y) = (x .ih (((adjh` S) +op (adjh` T))` y)))
50	49	ex 373	. . 3 |- ((S e. dom adjh /\ T e. dom adjh) -> ((x e. H~ /\ y e. H~) -> (((S +op T)` x) .ih y)