volioofmpt - Mathbox for Glauco Siliprandi

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

Theorem volioofmpt 45954

Description: ((vol ∘ (,)) ∘ 𝐹) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

**Hypotheses**
Ref	Expression
volioofmpt.x	⊢ Ⅎ𝑥𝐹
volioofmpt.f	⊢ (𝜑 → 𝐹:𝐴⟶(ℝ^* × ℝ^*))

**Assertion**
Ref	Expression
volioofmpt	⊢ (𝜑 → ((vol ∘ (,)) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (vol‘((1^st ‘(𝐹‘𝑥))(,)(2^nd ‘(𝐹‘𝑥))))))

Distinct variable groups: 𝑥,𝐴 𝜑,𝑥 Allowed substitution hint: 𝐹(𝑥)

**Proof of Theorem volioofmpt**
Step	Hyp	Ref	Expression
1		nfcv 2897	. . 3 ⊢ Ⅎ𝑥𝐴
2		nfcv 2897	. . . 4 ⊢ Ⅎ𝑥(vol ∘ (,))
3		volioofmpt.x	. . . 4 ⊢ Ⅎ𝑥𝐹
4	2, 3	nfco 5858	. . 3 ⊢ Ⅎ𝑥((vol ∘ (,)) ∘ 𝐹)
5		volioof 45947	. . . . 5 ⊢ (vol ∘ (,)):(ℝ^* × ℝ^*)⟶(0[,]+∞)
6	5	a1i 11	. . . 4 ⊢ (𝜑 → (vol ∘ (,)):(ℝ^* × ℝ^*)⟶(0[,]+∞))
7		volioofmpt.f	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶(ℝ^* × ℝ^*))
8		fco 6741	. . . 4 ⊢ (((vol ∘ (,)):(ℝ^* × ℝ^)⟶(0[,]+∞) ∧ 𝐹:𝐴⟶(ℝ^ × ℝ^*)) → ((vol ∘ (,)) ∘ 𝐹):𝐴⟶(0[,]+∞))
9	6, 7, 8	syl2anc 584	. . 3 ⊢ (𝜑 → ((vol ∘ (,)) ∘ 𝐹):𝐴⟶(0[,]+∞))
10	1, 4, 9	feqmptdf 6960	. 2 ⊢ (𝜑 → ((vol ∘ (,)) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (((vol ∘ (,)) ∘ 𝐹)‘𝑥)))
11	7	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹:𝐴⟶(ℝ^* × ℝ^*))
12		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
13	11, 12	fvvolioof 45949	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((vol ∘ (,)) ∘ 𝐹)‘𝑥) = (vol‘((1^st ‘(𝐹‘𝑥))(,)(2^nd ‘(𝐹‘𝑥)))))
14	13	mpteq2dva 5224	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((vol ∘ (,)) ∘ 𝐹)‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (vol‘((1^st ‘(𝐹‘𝑥))(,)(2^nd ‘(𝐹‘𝑥))))))
15	10, 14	eqtrd 2769	1 ⊢ (𝜑 → ((vol ∘ (,)) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (vol‘((1^st ‘(𝐹‘𝑥))(,)(2^nd ‘(𝐹‘𝑥))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2107 Ⅎwnfc 2882 ↦ cmpt 5207 × cxp 5665 ∘ ccom 5671 ⟶wf 6538 ‘cfv 6542 (class class class)co 7414 1^st c1st 7995 2^nd c2nd 7996 0cc0 11138 +∞cpnf 11275 ℝ^*cxr 11277 (,)cioo 13370 [,]cicc 13373 volcvol 25453

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5261 ax-sep 5278 ax-nul 5288 ax-pow 5347 ax-pr 5414 ax-un 7738 ax-inf2 9664 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3773 df-csb 3882 df-dif 3936 df-un 3938 df-in 3940 df-ss 3950 df-pss 3953 df-nul 4316 df-if 4508 df-pw 4584 df-sn 4609 df-pr 4611 df-op 4615 df-uni 4890 df-int 4929 df-iun 4975 df-br 5126 df-opab 5188 df-mpt 5208 df-tr 5242 df-id 5560 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-pred 6303 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7680 df-om 7871 df-1st 7997 df-2nd 7998 df-frecs 8289 df-wrecs 8320 df-recs 8394 df-rdg 8433 df-1o 8489 df-2o 8490 df-er 8728 df-map 8851 df-pm 8852 df-en 8969 df-dom 8970 df-sdom 8971 df-fin 8972 df-sup 9465 df-inf 9466 df-oi 9533 df-dju 9924 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11477 df-neg 11478 df-div 11904 df-nn 12250 df-2 12312 df-3 12313 df-n0 12511 df-z 12598 df-uz 12862 df-q 12974 df-rp 13018 df-xadd 13138 df-ioo 13374 df-ico 13376 df-icc 13377 df-fz 13531 df-fzo 13678 df-fl 13815 df-seq 14026 df-exp 14086 df-hash 14353 df-cj 15121 df-re 15122 df-im 15123 df-sqrt 15257 df-abs 15258 df-clim 15507 df-rlim 15508 df-sum 15706 df-xmet 21324 df-met 21325 df-ovol 25454 df-vol 25455

This theorem is referenced by: ovolval5lem2 46613

W3C validator