Metamath Proof Explorer

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 ⊢ A ∈ − π π ∧ B ∈ − π π → A = B ↔ inftyexpi ⁡ A = inftyexpi ⁡ B

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ A = B → inftyexpi ⁡ A = inftyexpi ⁡ B
2 fveq2 ⊢ inftyexpi ⁡ A = inftyexpi ⁡ B → 1 st ⁡ inftyexpi ⁡ A = 1 st ⁡ inftyexpi ⁡ B
3 bj-inftyexpiinv ⊢ A ∈ − π π → 1 st ⁡ inftyexpi ⁡ A = A
4 3 adantr ⊢ A ∈ − π π ∧ B ∈ − π π → 1 st ⁡ inftyexpi ⁡ A = A
5 4 eqeq1d ⊢ A ∈ − π π ∧ B ∈ − π π → 1 st ⁡ inftyexpi ⁡ A = 1 st ⁡ inftyexpi ⁡ B ↔ A = 1 st ⁡ inftyexpi ⁡ B
6 5 biimpd ⊢ A ∈ − π π ∧ B ∈ − π π → 1 st ⁡ inftyexpi ⁡ A = 1 st ⁡ inftyexpi ⁡ B → A = 1 st ⁡ inftyexpi ⁡ B
7 bj-inftyexpiinv ⊢ B ∈ − π π → 1 st ⁡ inftyexpi ⁡ B = B
8 7 adantl ⊢ A ∈ − π π ∧ B ∈ − π π → 1 st ⁡ inftyexpi ⁡ B = B
9 8 eqeq2d ⊢ A ∈ − π π ∧ B ∈ − π π → A = 1 st ⁡ inftyexpi ⁡ B ↔ A = B
10 6 9 sylibd ⊢ A ∈ − π π ∧ B ∈ − π π → 1 st ⁡ inftyexpi ⁡ A = 1 st ⁡ inftyexpi ⁡ B → A = B
11 2 10 syl5 ⊢ A ∈ − π π ∧ B ∈ − π π → inftyexpi ⁡ A = inftyexpi ⁡ B → A = B
12 1 11 impbid2 ⊢ A ∈ − π π ∧ B ∈ − π π → A = B ↔ inftyexpi ⁡ A = inftyexpi ⁡ B