Theorem sitmfval 32029

Description: Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018.)

Hypotheses

Ref	Expression
sitmval.d	⊢ 𝐷 = (dist‘𝑊)
sitmval.1	⊢ (𝜑 → 𝑊 ∈ 𝑉)
sitmval.2	⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
sitmfval.1	⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
sitmfval.2	⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))

Assertion

Ref	Expression
sitmfval	⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) = (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝐹 ∘f 𝐷𝐺)))

Proof of Theorem sitmfval

Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sitmval.d	. . 3 ⊢ 𝐷 = (dist‘𝑊)
2		sitmval.1	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝑉)
3		sitmval.2	. . 3 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
4	1, 2, 3	sitmval 32028	. 2 ⊢ (𝜑 → (𝑊sitm𝑀) = (𝑓 ∈ dom (𝑊sitg𝑀), 𝑔 ∈ dom (𝑊sitg𝑀) ↦ (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔))))
5		simprl 771	. . . 4 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → 𝑓 = 𝐹)
6		simprr 773	. . . 4 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → 𝑔 = 𝐺)
7	5, 6	oveq12d 7231	. . 3 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (𝑓 ∘f 𝐷𝑔) = (𝐹 ∘f 𝐷𝐺))
8	7	fveq2d 6721	. 2 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝑓 ∘f 𝐷𝑔)) = (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝐹 ∘f 𝐷𝐺)))
9		sitmfval.1	. 2 ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
10		sitmfval.2	. 2 ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))
11		fvexd 6732	. 2 ⊢ (𝜑 → (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝐹 ∘f 𝐷𝐺)) ∈ V)
12	4, 8, 9, 10, 11	ovmpod 7361	1 ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) = (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝐹 ∘f 𝐷𝐺)))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110  Vcvv 3408  ∪ cuni 4819  dom cdm 5551  ran crn 5552  ‘cfv 6380  (class class class)co 7213   ∘_f cof 7467  0cc0 10729  +∞cpnf 10864  [,]cicc 12938   ↾_s cress 16784  distcds 16811  ℝ^*_𝑠cxrs 17005  measurescmeas 31875  sitmcsitm 32007  sitgcsitg 32008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-1st 7761  df-2nd 7762  df-sitm 32010

This theorem is referenced by:  sitmcl  32030  sitmf  32031