# Metamath Proof Explorer

Description: Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006) (Proof shortened by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Assertion adjvalval ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({A}\right)=\left(\iota {w}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}\right)$

### Proof

Step Hyp Ref Expression
1 adjcl ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({A}\right)\in ℋ$
2 eqcom ${⊢}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}↔{x}{\cdot }_{\mathrm{ih}}{w}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}$
3 adj2 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {A}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)$
4 3 3com23 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)$
5 4 3expa ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {x}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)$
6 5 eqeq2d ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{w}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}↔{x}{\cdot }_{\mathrm{ih}}{w}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)\right)$
7 2 6 syl5bb ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}↔{x}{\cdot }_{\mathrm{ih}}{w}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)\right)$
8 7 ralbidva ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{w}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)\right)$
9 8 adantr ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{w}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)\right)$
10 simpr ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {w}\in ℋ\right)\to {w}\in ℋ$
11 1 adantr ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {w}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({A}\right)\in ℋ$
12 hial2eq2 ${⊢}\left({w}\in ℋ\wedge {adj}_{h}\left({T}\right)\left({A}\right)\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{w}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)↔{w}={adj}_{h}\left({T}\right)\left({A}\right)\right)$
13 10 11 12 syl2anc ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{w}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({A}\right)↔{w}={adj}_{h}\left({T}\right)\left({A}\right)\right)$
14 9 13 bitrd ${⊢}\left(\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}↔{w}={adj}_{h}\left({T}\right)\left({A}\right)\right)$
15 1 14 riota5 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\to \left(\iota {w}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}\right)={adj}_{h}\left({T}\right)\left({A}\right)$
16 15 eqcomd ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({A}\right)=\left(\iota {w}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{w}\right)$