Theorem bj-inftyexpiinj

Description: Injectivity of the parameterization inftyexpi . Remark: a more conceptual proof would use bj-inftyexpiinv and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	bj-inftyexpiinj	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( 𝐴 = 𝐵 ↔ ( +∞ei ‘ 𝐴 ) = ( +∞ei ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐴 = 𝐵 → ( +∞ei ‘ 𝐴 ) = ( +∞ei ‘ 𝐵 ) )
2		fveq2	⊢ ( ( +∞ei ‘ 𝐴 ) = ( +∞ei ‘ 𝐵 ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) )
3		bj-inftyexpiinv	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = 𝐴 )
4	3	adantr	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = 𝐴 )
5	4	eqeq1d	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) ↔ 𝐴 = ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) ) )
6	5	biimpd	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) → 𝐴 = ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) ) )
7		bj-inftyexpiinv	⊢ ( 𝐵 ∈ ( - π (,] π ) → ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) = 𝐵 )
8	7	adantl	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) = 𝐵 )
9	8	eqeq2d	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( 𝐴 = ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
10	6 9	sylibd	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = ( 1st ‘ ( +∞ei ‘ 𝐵 ) ) → 𝐴 = 𝐵 ) )
11	2 10	syl5	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( ( +∞ei ‘ 𝐴 ) = ( +∞ei ‘ 𝐵 ) → 𝐴 = 𝐵 ) )
12	1 11	impbid2	⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐵 ∈ ( - π (,] π ) ) → ( 𝐴 = 𝐵 ↔ ( +∞ei ‘ 𝐴 ) = ( +∞ei ‘ 𝐵 ) ) )