# Metamath Proof Explorer

Description: The adjoint of the sum of two operators. Theorem 3.11(iii) of Beran p. 106. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjadd ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to {adj}_{h}\left({S}{+}_{\mathrm{op}}{T}\right)={adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 dmadjop ${⊢}{S}\in \mathrm{dom}{adj}_{h}\to {S}:ℋ⟶ℋ$
2 dmadjop ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {T}:ℋ⟶ℋ$
3 hoaddcl ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
4 1 2 3 syl2an ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
5 dmadjrn ${⊢}{S}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({S}\right)\in \mathrm{dom}{adj}_{h}$
6 dmadjop ${⊢}{adj}_{h}\left({S}\right)\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({S}\right):ℋ⟶ℋ$
7 5 6 syl ${⊢}{S}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({S}\right):ℋ⟶ℋ$
8 dmadjrn ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}$
9 dmadjop ${⊢}{adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right):ℋ⟶ℋ$
10 8 9 syl ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right):ℋ⟶ℋ$
11 hoaddcl ${⊢}\left({adj}_{h}\left({S}\right):ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\right)\to \left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right):ℋ⟶ℋ$
12 7 10 11 syl2an ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right):ℋ⟶ℋ$
13 adj2 ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {S}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)$
14 13 3expb ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {S}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)$
15 14 adantlr ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {S}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)$
16 adj2 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)$
17 16 3expb ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)$
18 17 adantll ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)$
19 15 18 oveq12d ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)=\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
20 1 ffvelrnda ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\right)\to {S}\left({x}\right)\in ℋ$
21 20 ad2ant2r ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {S}\left({x}\right)\in ℋ$
22 2 ffvelrnda ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
23 22 ad2ant2lr ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({x}\right)\in ℋ$
24 simprr ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {y}\in ℋ$
25 ax-his2 ${⊢}\left({S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)\to \left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}=\left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
26 21 23 24 25 syl3anc ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}=\left({S}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
27 simprl ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}\in ℋ$
28 adjcl ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {y}\in ℋ\right)\to {adj}_{h}\left({S}\right)\left({y}\right)\in ℋ$
29 28 ad2ant2rl ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {adj}_{h}\left({S}\right)\left({y}\right)\in ℋ$
30 adjcl ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {y}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({y}\right)\in ℋ$
31 30 ad2ant2l ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {adj}_{h}\left({T}\right)\left({y}\right)\in ℋ$
32 his7 ${⊢}\left({x}\in ℋ\wedge {adj}_{h}\left({S}\right)\left({y}\right)\in ℋ\wedge {adj}_{h}\left({T}\right)\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
33 27 29 31 32 syl3anc ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
34 19 26 33 3eqtr4rd ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)=\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
35 7 10 anim12i ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \left({adj}_{h}\left({S}\right):ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\right)$
36 hosval ${⊢}\left({adj}_{h}\left({S}\right):ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)={adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
37 36 3expa ${⊢}\left(\left({adj}_{h}\left({S}\right):ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\right)\wedge {y}\in ℋ\right)\to \left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)={adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
38 35 37 sylan ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge {y}\in ℋ\right)\to \left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)={adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
39 38 adantrl ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)={adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)$
40 39 oveq2d ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right)\left({y}\right){+}_{ℎ}{adj}_{h}\left({T}\right)\left({y}\right)\right)$
41 1 2 anim12i ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)$
42 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
43 42 3expa ${⊢}\left(\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
44 41 43 sylan ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge {x}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
45 44 adantrr ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
46 45 oveq1d ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
47 34 40 46 3eqtr4rd ${⊢}\left(\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)$
48 47 ralrimivva ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)$
49 adjeq ${⊢}\left(\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)\right)\left({y}\right)\right)\to {adj}_{h}\left({S}{+}_{\mathrm{op}}{T}\right)={adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)$
50 4 12 48 49 syl3anc ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to {adj}_{h}\left({S}{+}_{\mathrm{op}}{T}\right)={adj}_{h}\left({S}\right){+}_{\mathrm{op}}{adj}_{h}\left({T}\right)$