Step |
Hyp |
Ref |
Expression |
1 |
|
cnmetcoval.d |
⊢ 𝐷 = ( abs ∘ − ) |
2 |
|
cnmetcoval.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℂ × ℂ ) ) |
3 |
|
cnmetcoval.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝐴 ) |
4 |
2 3
|
fvovco |
⊢ ( 𝜑 → ( ( 𝐷 ∘ 𝐹 ) ‘ 𝐵 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) 𝐷 ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) |
5 |
2 3
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( ℂ × ℂ ) ) |
6 |
|
xp1st |
⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( ℂ × ℂ ) → ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ ) |
7 |
5 6
|
syl |
⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ ) |
8 |
|
xp2nd |
⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( ℂ × ℂ ) → ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ ) |
9 |
5 8
|
syl |
⊢ ( 𝜑 → ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ ) |
10 |
1
|
cnmetdval |
⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) 𝐷 ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) − ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) ) |
11 |
7 9 10
|
syl2anc |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) 𝐷 ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) − ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) ) |
12 |
4 11
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝐷 ∘ 𝐹 ) ‘ 𝐵 ) = ( abs ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝐵 ) ) − ( 2nd ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) ) |