sitmf - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sitmf		Structured version Visualization version GIF version

Theorem sitmf 34689

Description: The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018.)

**Hypotheses**
Ref	Expression
sitmf.0	⊢ (𝜑 → 𝑊 ∈ Mnd)
sitmf.1	⊢ (𝜑 → 𝑊 ∈ ∞MetSp)
sitmf.2	⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)

**Assertion**
Ref	Expression
sitmf	⊢ (𝜑 → (𝑊sitm𝑀):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞))

Proof of Theorem sitmf Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2769	. . . . . 6 ⊢ (dist‘𝑊) = (dist‘𝑊)
2		sitmf.1	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ ∞MetSp)
3	2	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → 𝑊 ∈ ∞MetSp)
4		sitmf.2	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
5	4	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → 𝑀 ∈ ∪ ran measures)
6		simprl 782	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → 𝑓 ∈ dom (𝑊sitg𝑀))
7		simprr 784	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → 𝑔 ∈ dom (𝑊sitg𝑀))
8	1, 3, 5, 6, 7	sitmfval 34687	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → (𝑓(𝑊sitm𝑀)𝑔) = (((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔)))
9		sitmf.0	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Mnd)
10	9	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → 𝑊 ∈ Mnd)
11	10, 3, 5, 6, 7	sitmcl 34688	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → (𝑓(𝑊sitm𝑀)𝑔) ∈ (0[,]+∞))
12	8, 11	eqeltrrd 2870	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ dom (𝑊sitg𝑀) ∧ 𝑔 ∈ dom (𝑊sitg𝑀))) → (((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔)) ∈ (0[,]+∞))
13	12	ralrimivva 3214	. . 3 ⊢ (𝜑 → ∀𝑓 ∈ dom (𝑊sitg𝑀)∀𝑔 ∈ dom (𝑊sitg𝑀)(((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔)) ∈ (0[,]+∞))
14		eqid 2769	. . . 4 ⊢ (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ^_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔))) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ^_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔)))
15	14	fmpo 8067	. . 3 ⊢ (∀𝑓 ∈ dom (𝑊sitg𝑀)∀𝑔 ∈ dom (𝑊sitg𝑀)(((ℝ^_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔)) ∈ (0[,]+∞) ↔ (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ^_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔))):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞))
16	13, 15	sylib 221	. 2 ⊢ (𝜑 → (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔))):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞))
17	1, 2, 4	sitmval 34686	. . 3 ⊢ (𝜑 → (𝑊sitm𝑀) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔))))
18	17	feq1d 6690	. 2 ⊢ (𝜑 → ((𝑊sitm𝑀):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞) ↔ (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝑓 ∘_f (dist‘𝑊)𝑔))):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞)))
19	16, 18	mpbird 260	1 ⊢ (𝜑 → (𝑊sitm𝑀):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2149 ∀wral 3085 ∪ cuni 4876 × cxp 5662 dom cdm 5664 ran crn 5665 ⟶wf 6535 ‘cfv 6539 (class class class)co 7413 ∈ cmpo 7415 ∘_f cof 7675 0cc0 11102 +∞cpnf 11242 [,]cicc 13377 ↾_s cress 17292 distcds 17321 ℝ^*_𝑠cxrs 17556 Mndcmnd 18794 ∞MetSpcxms 24445 measurescmeas 34532 sitmcsitm 34665 sitgcsitg 34666

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5273 ax-pow 5339 ax-pr 5407 ax-un 7735 ax-inf2 9612 ax-ac2 10449 ax-cnex 11158 ax-resscn 11159 ax-1cn 11160 ax-icn 11161 ax-addcl 11162 ax-addrcl 11163 ax-mulcl 11164 ax-mulrcl 11165 ax-mulcom 11166 ax-addass 11167 ax-mulass 11168 ax-distr 11169 ax-i2m1 11170 ax-1ne0 11171 ax-1rid 11172 ax-rnegex 11173 ax-rrecex 11174 ax-cnre 11175 ax-pre-lttri 11176 ax-pre-lttrn 11177 ax-pre-ltadd 11178 ax-pre-mulgt0 11179 ax-pre-sup 11180 ax-addf 11181 ax-mulf 11182 ax-xrssca 33267 ax-xrsvsca 33268

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-disj 5081 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5559 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-pred 6305 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6495 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7677 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-tpos 8224 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9324 df-fi 9373 df-sup 9404 df-inf 9405 df-oi 9474 df-dju 9889 df-card 9927 df-acn 9930 df-ac 10102 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11445 df-neg 11446 df-div 11874 df-nn 12236 df-2 12305 df-3 12306 df-4 12307 df-5 12308 df-6 12309 df-7 12310 df-8 12311 df-9 12312 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12865 df-q 12975 df-rp 13019 df-xneg 13139 df-xadd 13140 df-xmul 13141 df-ioo 13378 df-ioc 13379 df-ico 13380 df-icc 13381 df-fz 13538 df-fzo 13685 df-fl 13827 df-mod 13905 df-seq 14040 df-exp 14100 df-fac 14312 df-bc 14341 df-hash 14369 df-shft 15106 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-limsup 15524 df-clim 15541 df-rlim 15542 df-sum 15740 df-ef 16123 df-sin 16125 df-cos 16126 df-pi 16128 df-dvds 16313 df-gcd 16555 df-numer 16796 df-denom 16797 df-gz 16992 df-struct 17209 df-sets 17226 df-slot 17244 df-ndx 17256 df-base 17272 df-ress 17293 df-plusg 17325 df-mulr 17326 df-starv 17327 df-sca 17328 df-vsca 17329 df-ip 17330 df-tset 17331 df-ple 17332 df-ds 17334 df-unif 17335 df-hom 17336 df-cco 17337 df-rest 17477 df-topn 17478 df-0g 17496 df-gsum 17497 df-topgen 17498 df-pt 17499 df-prds 17502 df-ordt 17557 df-xrs 17558 df-qtop 17563 df-imas 17564 df-xps 17566 df-mre 17640 df-mrc 17641 df-acs 17643 df-proset 18352 df-poset 18371 df-plt 18386 df-toset 18473 df-ps 18624 df-tsr 18625 df-plusf 18699 df-mgm 18700 df-sgrp 18779 df-mnd 18795 df-mhm 18843 df-submnd 18844 df-grp 19005 df-minusg 19006 df-sbg 19007 df-mulg 19136 df-subg 19191 df-ghm 19286 df-cntz 19389 df-od 19600 df-cmn 19854 df-abl 19855 df-omnd 20193 df-ogrp 20194 df-mgp 20219 df-rng 20233 df-ur 20266 df-ring 20319 df-cring 20320 df-oppr 20421 df-dvdsr 20441 df-unit 20442 df-invr 20472 df-dvr 20485 df-rhm 20556 df-nzr 20598 df-subrng 20633 df-subrg 20657 df-drng 20817 df-field 20818 df-abv 20892 df-orng 20942 df-ofld 20943 df-lmod 20963 df-scaf 20964 df-sra 21274 df-rgmod 21275 df-psmet 21485 df-xmet 21486 df-met 21487 df-bl 21488 df-mopn 21489 df-fbas 21490 df-fg 21491 df-metu 21492 df-cnfld 21494 df-zring 21568 df-zrh 21624 df-zlm 21625 df-chr 21626 df-refld 21726 df-top 23022 df-topon 23039 df-topsp 23061 df-bases 23074 df-cld 23147 df-ntr 23148 df-cls 23149 df-nei 23226 df-lp 23264 df-perf 23265 df-cn 23355 df-cnp 23356 df-t1 23442 df-haus 23443 df-reg 23444 df-cmp 23515 df-tx 23690 df-hmeo 23883 df-fil 23974 df-fm 24066 df-flim 24067 df-flf 24068 df-fcls 24069 df-cnext 24188 df-tmd 24200 df-tgp 24201 df-tsms 24255 df-trg 24288 df-ust 24329 df-utop 24359 df-uss 24384 df-usp 24385 df-ucn 24403 df-cfilu 24414 df-cusp 24425 df-xms 24448 df-ms 24449 df-tms 24450 df-nm 24710 df-ngp 24711 df-nrg 24713 df-nlm 24714 df-ii 25007 df-cncf 25008 df-cfil 25385 df-cmet 25387 df-cms 25465 df-limc 25996 df-dv 25997 df-log 26689 df-qqh 34308 df-rrh 34332 df-rrext 34336 df-esum 34365 df-siga 34446 df-sigagen 34476 df-meas 34533 df-mbfm 34587 df-sitg 34667 df-sitm 34668

This theorem is referenced by: (None)

W3C validator