itgmulc2

Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	itgmulc2.1	$⊢ φ \to C \in ℂ$
	itgmulc2.2	$⊢ (φ \land x \in A) \to B \in V$
	itgmulc2.3	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
Assertion	itgmulc2	$⊢ φ \to C \int_{A} B d x = \int_{A} C B d x$

Proof

Step	Hyp	Ref	Expression
1		itgmulc2.1	$⊢ φ \to C \in ℂ$
2		itgmulc2.2	$⊢ (φ \land x \in A) \to B \in V$
3		itgmulc2.3	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
4	1	recld	$⊢ φ \to ℜ (C) \in ℝ$
5	4	recnd	$⊢ φ \to ℜ (C) \in ℂ$
6	5	adantr	$⊢ (φ \land x \in A) \to ℜ (C) \in ℂ$
7		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
8	3 7	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
9	8 2	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
10	9	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
11	10	recnd	$⊢ (φ \land x \in A) \to ℜ (B) \in ℂ$
12	6 11	mulcld	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) \in ℂ$
13	9	iblcn	$⊢ φ \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1}))$
14	3 13	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1})$
15	14	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in 𝐿^{1}$
16	5 10 15	iblmulc2	$⊢ φ \to (x \in A ⟼ ℜ (C) ℜ (B)) \in 𝐿^{1}$
17	12 16	itgcl	$⊢ φ \to \int_{A} ℜ (C) ℜ (B) d x \in ℂ$
18		ax-icn	$⊢ i \in ℂ$
19	9	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
20	19	recnd	$⊢ (φ \land x \in A) \to ℑ (B) \in ℂ$
21	6 20	mulcld	$⊢ (φ \land x \in A) \to ℜ (C) ℑ (B) \in ℂ$
22	14	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in 𝐿^{1}$
23	5 19 22	iblmulc2	$⊢ φ \to (x \in A ⟼ ℜ (C) ℑ (B)) \in 𝐿^{1}$
24	21 23	itgcl	$⊢ φ \to \int_{A} ℜ (C) ℑ (B) d x \in ℂ$
25		mulcl	$⊢ (i \in ℂ \land \int_{A} ℜ (C) ℑ (B) d x \in ℂ) \to i \int_{A} ℜ (C) ℑ (B) d x \in ℂ$
26	18 24 25	sylancr	$⊢ φ \to i \int_{A} ℜ (C) ℑ (B) d x \in ℂ$
27	1	imcld	$⊢ φ \to ℑ (C) \in ℝ$
28	27	renegcld	$⊢ φ \to - ℑ (C) \in ℝ$
29	28	recnd	$⊢ φ \to - ℑ (C) \in ℂ$
30	29	adantr	$⊢ (φ \land x \in A) \to - ℑ (C) \in ℂ$
31	30 20	mulcld	$⊢ (φ \land x \in A) \to (- ℑ (C)) ℑ (B) \in ℂ$
32	29 19 22	iblmulc2	$⊢ φ \to (x \in A ⟼ (- ℑ (C)) ℑ (B)) \in 𝐿^{1}$
33	31 32	itgcl	$⊢ φ \to \int_{A} (- ℑ (C)) ℑ (B) d x \in ℂ$
34	27	recnd	$⊢ φ \to ℑ (C) \in ℂ$
35	34	adantr	$⊢ (φ \land x \in A) \to ℑ (C) \in ℂ$
36	35 11	mulcld	$⊢ (φ \land x \in A) \to ℑ (C) ℜ (B) \in ℂ$
37	34 10 15	iblmulc2	$⊢ φ \to (x \in A ⟼ ℑ (C) ℜ (B)) \in 𝐿^{1}$
38	36 37	itgcl	$⊢ φ \to \int_{A} ℑ (C) ℜ (B) d x \in ℂ$
39		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (C) ℜ (B) d x \in ℂ) \to i \int_{A} ℑ (C) ℜ (B) d x \in ℂ$
40	18 38 39	sylancr	$⊢ φ \to i \int_{A} ℑ (C) ℜ (B) d x \in ℂ$
41	17 26 33 40	add4d	$⊢ φ \to \int_{A} ℜ (C) ℜ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x = \int_{A} ℜ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
42	2 3	itgcl	$⊢ φ \to \int_{A} B d x \in ℂ$
43		mulcl	$⊢ (i \in ℂ \land ℑ (C) \in ℂ) \to i ℑ (C) \in ℂ$
44	18 34 43	sylancr	$⊢ φ \to i ℑ (C) \in ℂ$
45	2 3	itgcnval	$⊢ φ \to \int_{A} B d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x$
46	45	oveq2d	$⊢ φ \to ℜ (C) \int_{A} B d x = ℜ (C) (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x)$
47	10 15	itgcl	$⊢ φ \to \int_{A} ℜ (B) d x \in ℂ$
48	19 22	itgcl	$⊢ φ \to \int_{A} ℑ (B) d x \in ℂ$
49		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (B) d x \in ℂ) \to i \int_{A} ℑ (B) d x \in ℂ$
50	18 48 49	sylancr	$⊢ φ \to i \int_{A} ℑ (B) d x \in ℂ$
51	5 47 50	adddid	$⊢ φ \to ℜ (C) (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x) = ℜ (C) \int_{A} ℜ (B) d x + ℜ (C) i \int_{A} ℑ (B) d x$
52	5 10 15 4 10	itgmulc2lem2	$⊢ φ \to ℜ (C) \int_{A} ℜ (B) d x = \int_{A} ℜ (C) ℜ (B) d x$
53	18	a1i	$⊢ φ \to i \in ℂ$
54	5 53 48	mul12d	$⊢ φ \to ℜ (C) i \int_{A} ℑ (B) d x = i ℜ (C) \int_{A} ℑ (B) d x$
55	5 19 22 4 19	itgmulc2lem2	$⊢ φ \to ℜ (C) \int_{A} ℑ (B) d x = \int_{A} ℜ (C) ℑ (B) d x$
56	55	oveq2d	$⊢ φ \to i ℜ (C) \int_{A} ℑ (B) d x = i \int_{A} ℜ (C) ℑ (B) d x$
57	54 56	eqtrd	$⊢ φ \to ℜ (C) i \int_{A} ℑ (B) d x = i \int_{A} ℜ (C) ℑ (B) d x$
58	52 57	oveq12d	$⊢ φ \to ℜ (C) \int_{A} ℜ (B) d x + ℜ (C) i \int_{A} ℑ (B) d x = \int_{A} ℜ (C) ℜ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x$
59	46 51 58	3eqtrd	$⊢ φ \to ℜ (C) \int_{A} B d x = \int_{A} ℜ (C) ℜ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x$
60	45	oveq2d	$⊢ φ \to i ℑ (C) \int_{A} B d x = i ℑ (C) (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x)$
61	44 47 50	adddid	$⊢ φ \to i ℑ (C) (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x) = i ℑ (C) \int_{A} ℜ (B) d x + i ℑ (C) i \int_{A} ℑ (B) d x$
62	53 34 47	mulassd	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x = i ℑ (C) \int_{A} ℜ (B) d x$
63	34 10 15 27 10	itgmulc2lem2	$⊢ φ \to ℑ (C) \int_{A} ℜ (B) d x = \int_{A} ℑ (C) ℜ (B) d x$
64	63	oveq2d	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x = i \int_{A} ℑ (C) ℜ (B) d x$
65	62 64	eqtrd	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x = i \int_{A} ℑ (C) ℜ (B) d x$
66	53 34 53 48	mul4d	$⊢ φ \to i ℑ (C) i \int_{A} ℑ (B) d x = i i ℑ (C) \int_{A} ℑ (B) d x$
67		ixi	$⊢ i i = - 1$
68	67	oveq1i	$⊢ i i ℑ (C) \int_{A} ℑ (B) d x = -1 ℑ (C) \int_{A} ℑ (B) d x$
69	34 48	mulcld	$⊢ φ \to ℑ (C) \int_{A} ℑ (B) d x \in ℂ$
70	69	mulm1d	$⊢ φ \to -1 ℑ (C) \int_{A} ℑ (B) d x = - ℑ (C) \int_{A} ℑ (B) d x$
71	68 70	eqtrid	$⊢ φ \to i i ℑ (C) \int_{A} ℑ (B) d x = - ℑ (C) \int_{A} ℑ (B) d x$
72	34 48	mulneg1d	$⊢ φ \to (- ℑ (C)) \int_{A} ℑ (B) d x = - ℑ (C) \int_{A} ℑ (B) d x$
73	29 19 22 28 19	itgmulc2lem2	$⊢ φ \to (- ℑ (C)) \int_{A} ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x$
74	72 73	eqtr3d	$⊢ φ \to - ℑ (C) \int_{A} ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x$
75	66 71 74	3eqtrd	$⊢ φ \to i ℑ (C) i \int_{A} ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x$
76	65 75	oveq12d	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x + i ℑ (C) i \int_{A} ℑ (B) d x = i \int_{A} ℑ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x$
77	40 33 76	comraddd	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x + i ℑ (C) i \int_{A} ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
78	60 61 77	3eqtrd	$⊢ φ \to i ℑ (C) \int_{A} B d x = \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
79	59 78	oveq12d	$⊢ φ \to ℜ (C) \int_{A} B d x + i ℑ (C) \int_{A} B d x = \int_{A} ℜ (C) ℜ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
80	5 42 44 79	joinlmuladdmuld	$⊢ φ \to (ℜ (C) + i ℑ (C)) \int_{A} B d x = \int_{A} ℜ (C) ℜ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
81	35 20	mulcld	$⊢ (φ \land x \in A) \to ℑ (C) ℑ (B) \in ℂ$
82	12 81	negsubd	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) + (- ℑ (C) ℑ (B)) = ℜ (C) ℜ (B) - ℑ (C) ℑ (B)$
83	35 20	mulneg1d	$⊢ (φ \land x \in A) \to (- ℑ (C)) ℑ (B) = - ℑ (C) ℑ (B)$
84	83	oveq2d	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B) = ℜ (C) ℜ (B) + (- ℑ (C) ℑ (B))$
85	1	adantr	$⊢ (φ \land x \in A) \to C \in ℂ$
86	85 9	remuld	$⊢ (φ \land x \in A) \to ℜ (C B) = ℜ (C) ℜ (B) - ℑ (C) ℑ (B)$
87	82 84 86	3eqtr4d	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B) = ℜ (C B)$
88	87	itgeq2dv	$⊢ φ \to \int_{A} (ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B)) d x = \int_{A} ℜ (C B) d x$
89	12 16 31 32	itgadd	$⊢ φ \to \int_{A} (ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B)) d x = \int_{A} ℜ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x$
90	88 89	eqtr3d	$⊢ φ \to \int_{A} ℜ (C B) d x = \int_{A} ℜ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x$
91	85 9	immuld	$⊢ (φ \land x \in A) \to ℑ (C B) = ℜ (C) ℑ (B) + ℑ (C) ℜ (B)$
92	91	itgeq2dv	$⊢ φ \to \int_{A} ℑ (C B) d x = \int_{A} (ℜ (C) ℑ (B) + ℑ (C) ℜ (B)) d x$
93	21 23 36 37	itgadd	$⊢ φ \to \int_{A} (ℜ (C) ℑ (B) + ℑ (C) ℜ (B)) d x = \int_{A} ℜ (C) ℑ (B) d x + \int_{A} ℑ (C) ℜ (B) d x$
94	92 93	eqtrd	$⊢ φ \to \int_{A} ℑ (C B) d x = \int_{A} ℜ (C) ℑ (B) d x + \int_{A} ℑ (C) ℜ (B) d x$
95	94	oveq2d	$⊢ φ \to i \int_{A} ℑ (C B) d x = i (\int_{A} ℜ (C) ℑ (B) d x + \int_{A} ℑ (C) ℜ (B) d x)$
96	53 24 38	adddid	$⊢ φ \to i (\int_{A} ℜ (C) ℑ (B) d x + \int_{A} ℑ (C) ℜ (B) d x) = i \int_{A} ℜ (C) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
97	95 96	eqtrd	$⊢ φ \to i \int_{A} ℑ (C B) d x = i \int_{A} ℜ (C) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
98	90 97	oveq12d	$⊢ φ \to \int_{A} ℜ (C B) d x + i \int_{A} ℑ (C B) d x = \int_{A} ℜ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
99	41 80 98	3eqtr4d	$⊢ φ \to (ℜ (C) + i ℑ (C)) \int_{A} B d x = \int_{A} ℜ (C B) d x + i \int_{A} ℑ (C B) d x$
100	1	replimd	$⊢ φ \to C = ℜ (C) + i ℑ (C)$
101	100	oveq1d	$⊢ φ \to C \int_{A} B d x = (ℜ (C) + i ℑ (C)) \int_{A} B d x$
102	85 9	mulcld	$⊢ (φ \land x \in A) \to C B \in ℂ$
103	1 2 3	iblmulc2	$⊢ φ \to (x \in A ⟼ C B) \in 𝐿^{1}$
104	102 103	itgcnval	$⊢ φ \to \int_{A} C B d x = \int_{A} ℜ (C B) d x + i \int_{A} ℑ (C B) d x$
105	99 101 104	3eqtr4d	$⊢ φ \to C \int_{A} B d x = \int_{A} C B d x$

Metamath Proof Explorer

Theorem itgmulc2

Proof