itgvallem3

		Ref	Expression
	Hypothesis	itgvallem3.1	$⊢ (φ \land x \in A) \to B = 0$
	Assertion	itgvallem3	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq B), B, 0))) = 0$

Step	Hyp	Ref	Expression
1		itgvallem3.1	$⊢ (φ \land x \in A) \to B = 0$
2	1	adantrr	$⊢ (φ \land (x \in A \land 0 \leq B)) \to B = 0$
3	2	ifeq1da	$⊢ φ \to if ((x \in A \land 0 \leq B), B, 0) = if ((x \in A \land 0 \leq B), 0, 0)$
4		ifid	$⊢ if ((x \in A \land 0 \leq B), 0, 0) = 0$
5	3 4	eqtrdi	$⊢ φ \to if ((x \in A \land 0 \leq B), B, 0) = 0$
6	5	mpteq2dv	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq B), B, 0)) = (x \in ℝ ⟼ 0)$
7		fconstmpt	$⊢ ℝ \times \{0\} = (x \in ℝ ⟼ 0)$
8	6 7	eqtr4di	$⊢ φ \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq B), B, 0)) = ℝ \times \{0\}$
9	8	fveq2d	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq B), B, 0))) = \int^{2} (ℝ \times \{0\})$
10		itg20	$⊢ \int^{2} (ℝ \times \{0\}) = 0$
11	9 10	eqtrdi	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq B), B, 0))) = 0$

Metamath Proof Explorer