cnmetcoval - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cnmetcoval		Structured version Visualization version GIF version

Theorem cnmetcoval 39923

Description: Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

**Hypotheses**
Ref	Expression
cnmetcoval.d	⊢ 𝐷 = (abs ∘ − )
cnmetcoval.f	⊢ (𝜑 → 𝐹:𝐴⟶(ℂ × ℂ))
cnmetcoval.b	⊢ (𝜑 → 𝐵 ∈ 𝐴)

**Assertion**
Ref	Expression
cnmetcoval	⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = (abs‘((1^st ‘(𝐹‘𝐵)) − (2^nd ‘(𝐹‘𝐵)))))

**Proof of Theorem cnmetcoval**
Step	Hyp	Ref	Expression
1		cnmetcoval.f	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶(ℂ × ℂ))
2		cnmetcoval.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
3	1, 2	fvovco 39912	. 2 ⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = ((1^st ‘(𝐹‘𝐵))𝐷(2^nd ‘(𝐹‘𝐵))))
4	1, 2	ffvelrnd 6520	. . . 4 ⊢ (𝜑 → (𝐹‘𝐵) ∈ (ℂ × ℂ))
5		xp1st 7368	. . . 4 ⊢ ((𝐹‘𝐵) ∈ (ℂ × ℂ) → (1^st ‘(𝐹‘𝐵)) ∈ ℂ)
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → (1^st ‘(𝐹‘𝐵)) ∈ ℂ)
7		xp2nd 7369	. . . 4 ⊢ ((𝐹‘𝐵) ∈ (ℂ × ℂ) → (2^nd ‘(𝐹‘𝐵)) ∈ ℂ)
8	4, 7	syl 17	. . 3 ⊢ (𝜑 → (2^nd ‘(𝐹‘𝐵)) ∈ ℂ)
9		cnmetcoval.d	. . . 4 ⊢ 𝐷 = (abs ∘ − )
10	9	cnmetdval 22814	. . 3 ⊢ (((1^st ‘(𝐹‘𝐵)) ∈ ℂ ∧ (2^nd ‘(𝐹‘𝐵)) ∈ ℂ) → ((1^st ‘(𝐹‘𝐵))𝐷(2^nd ‘(𝐹‘𝐵))) = (abs‘((1^st ‘(𝐹‘𝐵)) − (2^nd ‘(𝐹‘𝐵)))))
11	6, 8, 10	syl2anc 574	. 2 ⊢ (𝜑 → ((1^st ‘(𝐹‘𝐵))𝐷(2^nd ‘(𝐹‘𝐵))) = (abs‘((1^st ‘(𝐹‘𝐵)) − (2^nd ‘(𝐹‘𝐵)))))
12	3, 11	eqtrd 2808	1 ⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = (abs‘((1^st ‘(𝐹‘𝐵)) − (2^nd ‘(𝐹‘𝐵)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1634 ∈ wcel 2148 × cxp 5261 ∘ ccom 5267 ⟶wf 6038 ‘cfv 6042 (class class class)co 6812 1^st c1st 7334 2^nd c2nd 7335 ℂcc 10157 − cmin 10489 abscabs 14204

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1873 ax-4 1888 ax-5 1994 ax-6 2060 ax-7 2096 ax-8 2150 ax-9 2157 ax-10 2177 ax-11 2193 ax-12 2206 ax-13 2411 ax-ext 2754 ax-sep 4928 ax-nul 4936 ax-pow 4988 ax-pr 5048 ax-un 7117 ax-resscn 10216 ax-1cn 10217 ax-icn 10218 ax-addcl 10219 ax-addrcl 10220 ax-mulcl 10221 ax-mulrcl 10222 ax-mulcom 10223 ax-addass 10224 ax-mulass 10225 ax-distr 10226 ax-i2m1 10227 ax-1ne0 10228 ax-1rid 10229 ax-rnegex 10230 ax-rrecex 10231 ax-cnre 10232 ax-pre-lttri 10233 ax-pre-lttrn 10234 ax-pre-ltadd 10235

This theorem depends on definitions: df-bi 198 df-an 384 df-or 864 df-3or 1099 df-3an 1100 df-tru 1637 df-ex 1856 df-nf 1861 df-sb 2053 df-eu 2625 df-mo 2626 df-clab 2761 df-cleq 2767 df-clel 2770 df-nfc 2905 df-ne 2947 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rab 3073 df-v 3357 df-sbc 3594 df-csb 3689 df-dif 3732 df-un 3734 df-in 3736 df-ss 3743 df-nul 4074 df-if 4236 df-pw 4309 df-sn 4327 df-pr 4329 df-op 4333 df-uni 4586 df-iun 4667 df-br 4798 df-opab 4860 df-mpt 4877 df-id 5171 df-po 5184 df-so 5185 df-xp 5269 df-rel 5270 df-cnv 5271 df-co 5272 df-dm 5273 df-rn 5274 df-res 5275 df-ima 5276 df-iota 6005 df-fun 6044 df-fn 6045 df-f 6046 df-f1 6047 df-fo 6048 df-f1o 6049 df-fv 6050 df-riota 6773 df-ov 6815 df-oprab 6816 df-mpt2 6817 df-1st 7336 df-2nd 7337 df-er 7917 df-en 8131 df-dom 8132 df-sdom 8133 df-pnf 10299 df-mnf 10300 df-ltxr 10302 df-sub 10491

This theorem is referenced by: (None)

W3C validator