Theorem bj-inftyexpiinv

Description: Utility theorem for the inverse of inftyexpi . (Contributed by BJ, 22-Jun-2019) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.)

	Ref	Expression
Assertion	bj-inftyexpiinv	$$⊢A\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\to 1^{st}\left(inftyexpi\left(A\right)\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$$⊢x=A\to ⟨x,ℂ⟩=⟨A,ℂ⟩$$
2		df-bj-inftyexpi	$$⊢inftyexpi=\left(x\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼⟨x,ℂ⟩\right)$$
3		opex	$$⊢⟨A,ℂ⟩\in \mathrm{V}$$
4	1 2 3	fvmpt	$$⊢A\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\to inftyexpi\left(A\right)=⟨A,ℂ⟩$$
5	4	fveq2d	$$⊢A\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\to 1^{st}\left(inftyexpi\left(A\right)\right)=1^{st}\left(⟨A,ℂ⟩\right)$$
6		cnex	$$⊢ℂ\in \mathrm{V}$$
7		op1stg	$$⊢\left(A\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\wedge ℂ\in \mathrm{V}\right)\to 1^{st}\left(⟨A,ℂ⟩\right)=A$$
8	6 7	mpan2	$$⊢A\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\to 1^{st}\left(⟨A,ℂ⟩\right)=A$$
9	5 8	eqtrd	$$⊢A\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\to 1^{st}\left(inftyexpi\left(A\right)\right)=A$$