3factsumint

Description: Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024)

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

Proof

Step	Hyp	Ref	Expression
1		3factsumint.1	$⊢ A = [L, U]$
2		3factsumint.2	$⊢ φ \to B \in Fin$
3		3factsumint.3	$⊢ φ \to L \in ℝ$
4		3factsumint.4	$⊢ φ \to U \in ℝ$
5		3factsumint.5	$⊢ φ \to (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ$
6		3factsumint.6	$⊢ (φ \land k \in B) \to G \in ℂ$
7		3factsumint.7	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) : A \underset{cn}{⟶} ℂ$
8		cncff	$⊢ (x \in A ⟼ F) : A \underset{cn}{⟶} ℂ \to (x \in A ⟼ F) : A ⟶ ℂ$
9	5 8	syl	$⊢ φ \to (x \in A ⟼ F) : A ⟶ ℂ$
10		eqid	$⊢ (x \in A ⟼ F) = (x \in A ⟼ F)$
11	10	fmpt	$⊢ \forall x \in A F \in ℂ \leftrightarrow (x \in A ⟼ F) : A ⟶ ℂ$
12	9 11	sylibr	$⊢ φ \to \forall x \in A F \in ℂ$
13	12	r19.21bi	$⊢ (φ \land x \in A) \to F \in ℂ$
14		cncff	$⊢ (x \in A ⟼ H) : A \underset{cn}{⟶} ℂ \to (x \in A ⟼ H) : A ⟶ ℂ$
15	7 14	syl	$⊢ (φ \land k \in B) \to (x \in A ⟼ H) : A ⟶ ℂ$
16		eqid	$⊢ (x \in A ⟼ H) = (x \in A ⟼ H)$
17	16	fmpt	$⊢ \forall x \in A H \in ℂ \leftrightarrow (x \in A ⟼ H) : A ⟶ ℂ$
18	15 17	sylibr	$⊢ (φ \land k \in B) \to \forall x \in A H \in ℂ$
19	18	r19.21bi	$⊢ ((φ \land k \in B) \land x \in A) \to H \in ℂ$
20		anass	$⊢ ((φ \land k \in B) \land x \in A) \leftrightarrow (φ \land (k \in B \land x \in A))$
21		ancom	$⊢ (k \in B \land x \in A) \leftrightarrow (x \in A \land k \in B)$
22	21	anbi2i	$⊢ (φ \land (k \in B \land x \in A)) \leftrightarrow (φ \land (x \in A \land k \in B))$
23	20 22	bitri	$⊢ ((φ \land k \in B) \land x \in A) \leftrightarrow (φ \land (x \in A \land k \in B))$
24	23	imbi1i	$⊢ (((φ \land k \in B) \land x \in A) \to H \in ℂ) \leftrightarrow ((φ \land (x \in A \land k \in B)) \to H \in ℂ)$
25	19 24	mpbi	$⊢ (φ \land (x \in A \land k \in B)) \to H \in ℂ$
26	2 13 6 25	3factsumint4	$⊢ φ \to \int_{A} \sum_{k \in B} F G H d x = \int_{A} F \sum_{k \in B} G H d x$
27	1 2 3 4 13 5 6 25 7	3factsumint1	$⊢ φ \to \int_{A} \sum_{k \in B} F G H d x = \sum_{k \in B} \int_{A} F G H d x$
28	26 27	eqtr3d	$⊢ φ \to \int_{A} F \sum_{k \in B} G H d x = \sum_{k \in B} \int_{A} F G H d x$
29	13 6 25	3factsumint2	$⊢ φ \to \sum_{k \in B} \int_{A} F G H d x = \sum_{k \in B} \int_{A} G F H d x$
30	1 3 4 13 5 6 25 7	3factsumint3	$⊢ φ \to \sum_{k \in B} \int_{A} G F H d x = \sum_{k \in B} G \int_{A} F H d x$
31	28 29 30	3eqtrd	$⊢ φ \to \int_{A} F \sum_{k \in B} G H d x = \sum_{k \in B} G \int_{A} F H d x$

Metamath Proof Explorer

Theorem 3factsumint

Proof