Step |
Hyp |
Ref |
Expression |
1 |
|
opeq1 |
⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , ℂ ⟩ = ⟨ 𝐴 , ℂ ⟩ ) |
2 |
|
df-bj-inftyexpi |
⊢ +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ ) |
3 |
|
opex |
⊢ ⟨ 𝐴 , ℂ ⟩ ∈ V |
4 |
1 2 3
|
fvmpt |
⊢ ( 𝐴 ∈ ( - π (,] π ) → ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ ) |
5 |
4
|
fveq2d |
⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = ( 1st ‘ ⟨ 𝐴 , ℂ ⟩ ) ) |
6 |
|
cnex |
⊢ ℂ ∈ V |
7 |
|
op1stg |
⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ℂ ∈ V ) → ( 1st ‘ ⟨ 𝐴 , ℂ ⟩ ) = 𝐴 ) |
8 |
6 7
|
mpan2 |
⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ⟨ 𝐴 , ℂ ⟩ ) = 𝐴 ) |
9 |
5 8
|
eqtrd |
⊢ ( 𝐴 ∈ ( - π (,] π ) → ( 1st ‘ ( +∞ei ‘ 𝐴 ) ) = 𝐴 ) |