# Metamath Proof Explorer

Description: Double adjoint. Theorem 3.11(iv) of Beran p. 106. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjadj ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({adj}_{h}\left({T}\right)\right)={T}$

### Proof

Step Hyp Ref Expression
1 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)$
2 dmadjrn ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}$
3 adj1 ${⊢}\left({adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)={adj}_{h}\left({adj}_{h}\left({T}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
4 2 3 syl3an1 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({y}\right)={adj}_{h}\left({adj}_{h}\left({T}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
5 1 4 eqtr2d ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {adj}_{h}\left({adj}_{h}\left({T}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
6 5 3expib ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {adj}_{h}\left({adj}_{h}\left({T}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
7 6 ralrimivv ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{adj}_{h}\left({adj}_{h}\left({T}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
8 dmadjrn ${⊢}{adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({adj}_{h}\left({T}\right)\right)\in \mathrm{dom}{adj}_{h}$
9 dmadjop ${⊢}{adj}_{h}\left({adj}_{h}\left({T}\right)\right)\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({adj}_{h}\left({T}\right)\right):ℋ⟶ℋ$
10 2 8 9 3syl ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({adj}_{h}\left({T}\right)\right):ℋ⟶ℋ$
11 dmadjop ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {T}:ℋ⟶ℋ$
12 hoeq1 ${⊢}\left({adj}_{h}\left({adj}_{h}\left({T}\right)\right):ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{adj}_{h}\left({adj}_{h}\left({T}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{adj}_{h}\left({adj}_{h}\left({T}\right)\right)={T}\right)$
13 10 11 12 syl2anc ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{adj}_{h}\left({adj}_{h}\left({T}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{adj}_{h}\left({adj}_{h}\left({T}\right)\right)={T}\right)$
14 7 13 mpbid ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({adj}_{h}\left({T}\right)\right)={T}$