3factsumint1

Description: Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024)

	Ref	Expression
Hypotheses	3factsumint1.1	$⊢ A = [L, U]$
	3factsumint1.2	$⊢ φ \to B \in Fin$
	3factsumint1.3	$⊢ φ \to L \in ℝ$
	3factsumint1.4	$⊢ φ \to U \in ℝ$
	3factsumint1.5	$⊢ (φ \land x \in A) \to F \in ℂ$
	3factsumint1.6	$⊢ φ \to (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ$
	3factsumint1.7	$⊢ (φ \land k \in B) \to G \in ℂ$
	3factsumint1.8	$⊢ (φ \land (x \in A \land k \in B)) \to H \in ℂ$
	3factsumint1.9	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) : A \underset{cn}{⟶} ℂ$
Assertion	3factsumint1	$⊢ φ \to \int_{A} \sum_{k \in B} F G H d x = \sum_{k \in B} \int_{A} F G H d x$

Proof

Step	Hyp	Ref	Expression
1		3factsumint1.1	$⊢ A = [L, U]$
2		3factsumint1.2	$⊢ φ \to B \in Fin$
3		3factsumint1.3	$⊢ φ \to L \in ℝ$
4		3factsumint1.4	$⊢ φ \to U \in ℝ$
5		3factsumint1.5	$⊢ (φ \land x \in A) \to F \in ℂ$
6		3factsumint1.6	$⊢ φ \to (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ$
7		3factsumint1.7	$⊢ (φ \land k \in B) \to G \in ℂ$
8		3factsumint1.8	$⊢ (φ \land (x \in A \land k \in B)) \to H \in ℂ$
9		3factsumint1.9	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) : A \underset{cn}{⟶} ℂ$
10		iccmbl	$⊢ (L \in ℝ \land U \in ℝ) \to [L, U] \in dom vol$
11	3 4 10	syl2anc	$⊢ φ \to [L, U] \in dom vol$
12	1 11	eqeltrid	$⊢ φ \to A \in dom vol$
13	5	adantrr	$⊢ (φ \land (x \in A \land k \in B)) \to F \in ℂ$
14	7	adantrl	$⊢ (φ \land (x \in A \land k \in B)) \to G \in ℂ$
15	14 8	mulcld	$⊢ (φ \land (x \in A \land k \in B)) \to G H \in ℂ$
16	13 15	mulcld	$⊢ (φ \land (x \in A \land k \in B)) \to F G H \in ℂ$
17		ovex	$⊢ [L, U] \in V$
18	1 17	eqeltri	$⊢ A \in V$
19	18	a1i	$⊢ (φ \land k \in B) \to A \in V$
20	13	anass1rs	$⊢ ((φ \land k \in B) \land x \in A) \to F \in ℂ$
21	15	anass1rs	$⊢ ((φ \land k \in B) \land x \in A) \to G H \in ℂ$
22		eqidd	$⊢ (φ \land k \in B) \to (x \in A ⟼ F) = (x \in A ⟼ F)$
23		eqidd	$⊢ (φ \land k \in B) \to (x \in A ⟼ G H) = (x \in A ⟼ G H)$
24	19 20 21 22 23	offval2	$⊢ (φ \land k \in B) \to (x \in A ⟼ F) \times_{f} (x \in A ⟼ G H) = (x \in A ⟼ F G H)$
25		cnmbf	$⊢ (A \in dom vol \land (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ) \to (x \in A ⟼ F) \in MblFn$
26	12 6 25	syl2anc	$⊢ φ \to (x \in A ⟼ F) \in MblFn$
27	26	adantr	$⊢ (φ \land k \in B) \to (x \in A ⟼ F) \in MblFn$
28	8	anass1rs	$⊢ ((φ \land k \in B) \land x \in A) \to H \in ℂ$
29	3	adantr	$⊢ (φ \land k \in B) \to L \in ℝ$
30	4	adantr	$⊢ (φ \land k \in B) \to U \in ℝ$
31	1	oveq1i	$⊢ A \underset{cn}{⟶} ℂ = [L, U] \underset{cn}{⟶} ℂ$
32	31	eleq2i	$⊢ (x \in A ⟼ H) : A \underset{cn}{⟶} ℂ \leftrightarrow (x \in A ⟼ H) : [L, U] \underset{cn}{⟶} ℂ$
33	9 32	sylib	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) : [L, U] \underset{cn}{⟶} ℂ$
34		cnicciblnc	$⊢ (L \in ℝ \land U \in ℝ \land (x \in A ⟼ H) : [L, U] \underset{cn}{⟶} ℂ) \to (x \in A ⟼ H) \in 𝐿^{1}$
35	29 30 33 34	syl3anc	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) \in 𝐿^{1}$
36	7 28 35	iblmulc2	$⊢ (φ \land k \in B) \to (x \in A ⟼ G H) \in 𝐿^{1}$
37	31	eleq2i	$⊢ (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ \leftrightarrow (x \in A ⟼ F) : [L, U] \underset{cn}{⟶} ℂ$
38	6 37	sylib	$⊢ φ \to (x \in A ⟼ F) : [L, U] \underset{cn}{⟶} ℂ$
39		cniccbdd	$⊢ (L \in ℝ \land U \in ℝ \land (x \in A ⟼ F) : [L, U] \underset{cn}{⟶} ℂ) \to \exists q \in ℝ \forall r \in [L, U] \|(x \in A ⟼ F) (r)\| \leq q$
40	3 4 38 39	syl3anc	$⊢ φ \to \exists q \in ℝ \forall r \in [L, U] \|(x \in A ⟼ F) (r)\| \leq q$
41	40	adantr	$⊢ (φ \land k \in B) \to \exists q \in ℝ \forall r \in [L, U] \|(x \in A ⟼ F) (r)\| \leq q$
42	5	ralrimiva	$⊢ φ \to \forall x \in A F \in ℂ$
43		dmmptg	$⊢ \forall x \in A F \in ℂ \to dom (x \in A ⟼ F) = A$
44	42 43	syl	$⊢ φ \to dom (x \in A ⟼ F) = A$
45	44 1	eqtrdi	$⊢ φ \to dom (x \in A ⟼ F) = [L, U]$
46	45	raleqdv	$⊢ φ \to (\forall r \in dom (x \in A ⟼ F) \|(x \in A ⟼ F) (r)\| \leq q \leftrightarrow \forall r \in [L, U] \|(x \in A ⟼ F) (r)\| \leq q)$
47	46	rexbidv	$⊢ φ \to (\exists q \in ℝ \forall r \in dom (x \in A ⟼ F) \|(x \in A ⟼ F) (r)\| \leq q \leftrightarrow \exists q \in ℝ \forall r \in [L, U] \|(x \in A ⟼ F) (r)\| \leq q)$
48	47	adantr	$⊢ (φ \land k \in B) \to (\exists q \in ℝ \forall r \in dom (x \in A ⟼ F) \|(x \in A ⟼ F) (r)\| \leq q \leftrightarrow \exists q \in ℝ \forall r \in [L, U] \|(x \in A ⟼ F) (r)\| \leq q)$
49	41 48	mpbird	$⊢ (φ \land k \in B) \to \exists q \in ℝ \forall r \in dom (x \in A ⟼ F) \|(x \in A ⟼ F) (r)\| \leq q$
50		bddmulibl	$⊢ ((x \in A ⟼ F) \in MblFn \land (x \in A ⟼ G H) \in 𝐿^{1} \land \exists q \in ℝ \forall r \in dom (x \in A ⟼ F) \|(x \in A ⟼ F) (r)\| \leq q) \to (x \in A ⟼ F) \times_{f} (x \in A ⟼ G H) \in 𝐿^{1}$
51	27 36 49 50	syl3anc	$⊢ (φ \land k \in B) \to (x \in A ⟼ F) \times_{f} (x \in A ⟼ G H) \in 𝐿^{1}$
52	24 51	eqeltrrd	$⊢ (φ \land k \in B) \to (x \in A ⟼ F G H) \in 𝐿^{1}$
53	12 2 16 52	itgfsum	$⊢ φ \to ((x \in A ⟼ \sum_{k \in B} F G H) \in 𝐿^{1} \land \int_{A} \sum_{k \in B} F G H d x = \sum_{k \in B} \int_{A} F G H d x)$
54	53	simprd	$⊢ φ \to \int_{A} \sum_{k \in B} F G H d x = \sum_{k \in B} \int_{A} F G H d x$

Metamath Proof Explorer

Theorem 3factsumint1

Proof