Theorem ajfun

Description: The adjoint function is a function. This is not immediately apparent from df-aj but results from the uniqueness shown by ajmoi . (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ajfun.5	$$⊢A=U\mathrm{adj}W$$
Assertion	ajfun	$$⊢\left(U\in {CPreHil}_{\mathrm{OLD}}\wedge W\in \mathrm{NrmCVec}\right)\to \mathrm{Fun}A$$

Proof

Step	Hyp	Ref	Expression
1		ajfun.5	$$⊢A=U\mathrm{adj}W$$
2		oveq1	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to U\mathrm{adj}W=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}W$$
3	1 2	eqtrid	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to A=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}W$$
4	3	funeqd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\mathrm{Fun}A\leftrightarrow \mathrm{Fun}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}W\right)\right)$$
5		oveq2	$$⊢W=if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}W=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
6	5	funeqd	$$⊢W=if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\mathrm{Fun}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}W\right)\leftrightarrow \mathrm{Fun}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)$$
7		eqid	$$⊢if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
8		elimphu	$$⊢if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\in {CPreHil}_{\mathrm{OLD}}$$
9		elimnvu	$$⊢if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\in \mathrm{NrmCVec}$$
10	7 8 9	ajfuni	$$⊢\mathrm{Fun}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\mathrm{adj}if\left(W\in \mathrm{NrmCVec},W,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
11	4 6 10	dedth2h	$$⊢\left(U\in {CPreHil}_{\mathrm{OLD}}\wedge W\in \mathrm{NrmCVec}\right)\to \mathrm{Fun}A$$