itgmulc2nc

Description: Choice-free analogue of itgmulc2 . (Contributed by Brendan Leahy, 19-Nov-2017)

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

Proof

Step	Hyp	Ref	Expression
1		itgmulc2nc.1	$⊢ φ \to C \in ℂ$
2		itgmulc2nc.2	$⊢ (φ \land x \in A) \to B \in V$
3		itgmulc2nc.3	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
4		itgmulc2nc.m	$⊢ φ \to (x \in A ⟼ C B) \in MblFn$
5	1	recld	$⊢ φ \to ℜ (C) \in ℝ$
6	5	recnd	$⊢ φ \to ℜ (C) \in ℂ$
7	6	adantr	$⊢ (φ \land x \in A) \to ℜ (C) \in ℂ$
8		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
9	3 8	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
10	9 2	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
11	10	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
12	11	recnd	$⊢ (φ \land x \in A) \to ℜ (B) \in ℂ$
13	7 12	mulcld	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) \in ℂ$
14	10	iblcn	$⊢ φ \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1}))$
15	3 14	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1})$
16	15	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in 𝐿^{1}$
17		ovexd	$⊢ (φ \land x \in A) \to C B \in V$
18	4 17	mbfdm2	$⊢ φ \to A \in dom vol$
19		fconstmpt	$⊢ A \times \{ℜ (C)\} = (x \in A ⟼ ℜ (C))$
20	19	a1i	$⊢ φ \to A \times \{ℜ (C)\} = (x \in A ⟼ ℜ (C))$
21		eqidd	$⊢ φ \to (x \in A ⟼ ℜ (B)) = (x \in A ⟼ ℜ (B))$
22	18 7 11 20 21	offval2	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) = (x \in A ⟼ ℜ (C) ℜ (B))$
23		iblmbf	$⊢ (x \in A ⟼ ℜ (B)) \in 𝐿^{1} \to (x \in A ⟼ ℜ (B)) \in MblFn$
24	16 23	syl	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in MblFn$
25	12	fmpttd	$⊢ φ \to (x \in A ⟼ ℜ (B)) : A ⟶ ℂ$
26	24 5 25	mbfmulc2re	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) \in MblFn$
27	22 26	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℜ (C) ℜ (B)) \in MblFn$
28	6 11 16 27	iblmulc2nc	$⊢ φ \to (x \in A ⟼ ℜ (C) ℜ (B)) \in 𝐿^{1}$
29	13 28	itgcl	$⊢ φ \to \int_{A} ℜ (C) ℜ (B) d x \in ℂ$
30		ax-icn	$⊢ i \in ℂ$
31	10	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
32	31	recnd	$⊢ (φ \land x \in A) \to ℑ (B) \in ℂ$
33	7 32	mulcld	$⊢ (φ \land x \in A) \to ℜ (C) ℑ (B) \in ℂ$
34	15	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in 𝐿^{1}$
35		eqidd	$⊢ φ \to (x \in A ⟼ ℑ (B)) = (x \in A ⟼ ℑ (B))$
36	18 7 31 20 35	offval2	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) = (x \in A ⟼ ℜ (C) ℑ (B))$
37		iblmbf	$⊢ (x \in A ⟼ ℑ (B)) \in 𝐿^{1} \to (x \in A ⟼ ℑ (B)) \in MblFn$
38	34 37	syl	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in MblFn$
39	32	fmpttd	$⊢ φ \to (x \in A ⟼ ℑ (B)) : A ⟶ ℂ$
40	38 5 39	mbfmulc2re	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) \in MblFn$
41	36 40	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℜ (C) ℑ (B)) \in MblFn$
42	6 31 34 41	iblmulc2nc	$⊢ φ \to (x \in A ⟼ ℜ (C) ℑ (B)) \in 𝐿^{1}$
43	33 42	itgcl	$⊢ φ \to \int_{A} ℜ (C) ℑ (B) d x \in ℂ$
44		mulcl	$⊢ (i \in ℂ \land \int_{A} ℜ (C) ℑ (B) d x \in ℂ) \to i \int_{A} ℜ (C) ℑ (B) d x \in ℂ$
45	30 43 44	sylancr	$⊢ φ \to i \int_{A} ℜ (C) ℑ (B) d x \in ℂ$
46	1	imcld	$⊢ φ \to ℑ (C) \in ℝ$
47	46	recnd	$⊢ φ \to ℑ (C) \in ℂ$
48	47	negcld	$⊢ φ \to - ℑ (C) \in ℂ$
49	48	adantr	$⊢ (φ \land x \in A) \to - ℑ (C) \in ℂ$
50	49 32	mulcld	$⊢ (φ \land x \in A) \to (- ℑ (C)) ℑ (B) \in ℂ$
51		fconstmpt	$⊢ A \times \{- ℑ (C)\} = (x \in A ⟼ - ℑ (C))$
52	51	a1i	$⊢ φ \to A \times \{- ℑ (C)\} = (x \in A ⟼ - ℑ (C))$
53	18 49 31 52 35	offval2	$⊢ φ \to (A \times \{- ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) = (x \in A ⟼ (- ℑ (C)) ℑ (B))$
54	46	renegcld	$⊢ φ \to - ℑ (C) \in ℝ$
55	38 54 39	mbfmulc2re	$⊢ φ \to (A \times \{- ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) \in MblFn$
56	53 55	eqeltrrd	$⊢ φ \to (x \in A ⟼ (- ℑ (C)) ℑ (B)) \in MblFn$
57	48 31 34 56	iblmulc2nc	$⊢ φ \to (x \in A ⟼ (- ℑ (C)) ℑ (B)) \in 𝐿^{1}$
58	50 57	itgcl	$⊢ φ \to \int_{A} (- ℑ (C)) ℑ (B) d x \in ℂ$
59	47	adantr	$⊢ (φ \land x \in A) \to ℑ (C) \in ℂ$
60	59 12	mulcld	$⊢ (φ \land x \in A) \to ℑ (C) ℜ (B) \in ℂ$
61		fconstmpt	$⊢ A \times \{ℑ (C)\} = (x \in A ⟼ ℑ (C))$
62	61	a1i	$⊢ φ \to A \times \{ℑ (C)\} = (x \in A ⟼ ℑ (C))$
63	18 59 11 62 21	offval2	$⊢ φ \to (A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) = (x \in A ⟼ ℑ (C) ℜ (B))$
64	24 46 25	mbfmulc2re	$⊢ φ \to (A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) \in MblFn$
65	63 64	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℑ (C) ℜ (B)) \in MblFn$
66	47 11 16 65	iblmulc2nc	$⊢ φ \to (x \in A ⟼ ℑ (C) ℜ (B)) \in 𝐿^{1}$
67	60 66	itgcl	$⊢ φ \to \int_{A} ℑ (C) ℜ (B) d x \in ℂ$
68		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (C) ℜ (B) d x \in ℂ) \to i \int_{A} ℑ (C) ℜ (B) d x \in ℂ$
69	30 67 68	sylancr	$⊢ φ \to i \int_{A} ℑ (C) ℜ (B) d x \in ℂ$
70	29 45 58 69	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$
71	30	a1i	$⊢ φ \to i \in ℂ$
72	71 47	mulcld	$⊢ φ \to i ℑ (C) \in ℂ$
73	2 3	itgcl	$⊢ φ \to \int_{A} B d x \in ℂ$
74	6 72 73	adddird	$⊢ φ \to (ℜ (C) + i ℑ (C)) \int_{A} B d x = ℜ (C) \int_{A} B d x + i ℑ (C) \int_{A} B d x$
75	2 3	itgcnval	$⊢ φ \to \int_{A} B d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x$
76	75	oveq2d	$⊢ φ \to ℜ (C) \int_{A} B d x = ℜ (C) (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x)$
77	11 16	itgcl	$⊢ φ \to \int_{A} ℜ (B) d x \in ℂ$
78	31 34	itgcl	$⊢ φ \to \int_{A} ℑ (B) d x \in ℂ$
79		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (B) d x \in ℂ) \to i \int_{A} ℑ (B) d x \in ℂ$
80	30 78 79	sylancr	$⊢ φ \to i \int_{A} ℑ (B) d x \in ℂ$
81	6 77 80	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$
82	6 11 16 27 5 11	itgmulc2nclem2	$⊢ φ \to ℜ (C) \int_{A} ℜ (B) d x = \int_{A} ℜ (C) ℜ (B) d x$
83	6 71 78	mul12d	$⊢ φ \to ℜ (C) i \int_{A} ℑ (B) d x = i ℜ (C) \int_{A} ℑ (B) d x$
84	6 31 34 41 5 31	itgmulc2nclem2	$⊢ φ \to ℜ (C) \int_{A} ℑ (B) d x = \int_{A} ℜ (C) ℑ (B) d x$
85	84	oveq2d	$⊢ φ \to i ℜ (C) \int_{A} ℑ (B) d x = i \int_{A} ℜ (C) ℑ (B) d x$
86	83 85	eqtrd	$⊢ φ \to ℜ (C) i \int_{A} ℑ (B) d x = i \int_{A} ℜ (C) ℑ (B) d x$
87	82 86	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$
88	76 81 87	3eqtrd	$⊢ φ \to ℜ (C) \int_{A} B d x = \int_{A} ℜ (C) ℜ (B) d x + i \int_{A} ℜ (C) ℑ (B) d x$
89	75	oveq2d	$⊢ φ \to i ℑ (C) \int_{A} B d x = i ℑ (C) (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x)$
90	72 77 80	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$
91	71 47 77	mulassd	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x = i ℑ (C) \int_{A} ℜ (B) d x$
92	47 11 16 65 46 11	itgmulc2nclem2	$⊢ φ \to ℑ (C) \int_{A} ℜ (B) d x = \int_{A} ℑ (C) ℜ (B) d x$
93	92	oveq2d	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x = i \int_{A} ℑ (C) ℜ (B) d x$
94	91 93	eqtrd	$⊢ φ \to i ℑ (C) \int_{A} ℜ (B) d x = i \int_{A} ℑ (C) ℜ (B) d x$
95	71 47 71 78	mul4d	$⊢ φ \to i ℑ (C) i \int_{A} ℑ (B) d x = i i ℑ (C) \int_{A} ℑ (B) d x$
96		ixi	$⊢ i i = - 1$
97	96	oveq1i	$⊢ i i ℑ (C) \int_{A} ℑ (B) d x = -1 ℑ (C) \int_{A} ℑ (B) d x$
98	47 78	mulcld	$⊢ φ \to ℑ (C) \int_{A} ℑ (B) d x \in ℂ$
99	98	mulm1d	$⊢ φ \to -1 ℑ (C) \int_{A} ℑ (B) d x = - ℑ (C) \int_{A} ℑ (B) d x$
100	97 99	eqtrid	$⊢ φ \to i i ℑ (C) \int_{A} ℑ (B) d x = - ℑ (C) \int_{A} ℑ (B) d x$
101	47 78	mulneg1d	$⊢ φ \to (- ℑ (C)) \int_{A} ℑ (B) d x = - ℑ (C) \int_{A} ℑ (B) d x$
102	48 31 34 56 54 31	itgmulc2nclem2	$⊢ φ \to (- ℑ (C)) \int_{A} ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x$
103	101 102	eqtr3d	$⊢ φ \to - ℑ (C) \int_{A} ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x$
104	95 100 103	3eqtrd	$⊢ φ \to i ℑ (C) i \int_{A} ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x$
105	94 104	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$
106	69 58	addcomd	$⊢ φ \to 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$
107	105 106	eqtrd	$⊢ φ \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$
108	89 90 107	3eqtrd	$⊢ φ \to i ℑ (C) \int_{A} B d x = \int_{A} (- ℑ (C)) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
109	88 108	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$
110	74 109	eqtrd	$⊢ φ \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$
111	59 32	mulcld	$⊢ (φ \land x \in A) \to ℑ (C) ℑ (B) \in ℂ$
112	18 59 31 62 35	offval2	$⊢ φ \to (A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) = (x \in A ⟼ ℑ (C) ℑ (B))$
113	38 46 39	mbfmulc2re	$⊢ φ \to (A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) \in MblFn$
114	112 113	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℑ (C) ℑ (B)) \in MblFn$
115	47 31 34 114	iblmulc2nc	$⊢ φ \to (x \in A ⟼ ℑ (C) ℑ (B)) \in 𝐿^{1}$
116	1	adantr	$⊢ (φ \land x \in A) \to C \in ℂ$
117	116 10	mulcld	$⊢ (φ \land x \in A) \to C B \in ℂ$
118		eqidd	$⊢ φ \to (x \in A ⟼ C B) = (x \in A ⟼ C B)$
119		ref	$⊢ ℜ : ℂ ⟶ ℝ$
120	119	a1i	$⊢ φ \to ℜ : ℂ ⟶ ℝ$
121	120	feqmptd	$⊢ φ \to ℜ = (k \in ℂ ⟼ ℜ (k))$
122		fveq2	$⊢ k = C B \to ℜ (k) = ℜ (C B)$
123	117 118 121 122	fmptco	$⊢ φ \to ℜ \circ (x \in A ⟼ C B) = (x \in A ⟼ ℜ (C B))$
124	116 10	remuld	$⊢ (φ \land x \in A) \to ℜ (C B) = ℜ (C) ℜ (B) - ℑ (C) ℑ (B)$
125	124	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℜ (C B)) = (x \in A ⟼ ℜ (C) ℜ (B) - ℑ (C) ℑ (B))$
126	123 125	eqtrd	$⊢ φ \to ℜ \circ (x \in A ⟼ C B) = (x \in A ⟼ ℜ (C) ℜ (B) - ℑ (C) ℑ (B))$
127	117	fmpttd	$⊢ φ \to (x \in A ⟼ C B) : A ⟶ ℂ$
128		ismbfcn	$⊢ (x \in A ⟼ C B) : A ⟶ ℂ \to ((x \in A ⟼ C B) \in MblFn \leftrightarrow (ℜ \circ (x \in A ⟼ C B) \in MblFn \land ℑ \circ (x \in A ⟼ C B) \in MblFn))$
129	127 128	syl	$⊢ φ \to ((x \in A ⟼ C B) \in MblFn \leftrightarrow (ℜ \circ (x \in A ⟼ C B) \in MblFn \land ℑ \circ (x \in A ⟼ C B) \in MblFn))$
130	4 129	mpbid	$⊢ φ \to (ℜ \circ (x \in A ⟼ C B) \in MblFn \land ℑ \circ (x \in A ⟼ C B) \in MblFn)$
131	130	simpld	$⊢ φ \to ℜ \circ (x \in A ⟼ C B) \in MblFn$
132	126 131	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℜ (C) ℜ (B) - ℑ (C) ℑ (B)) \in MblFn$
133	13 28 111 115 132	itgsubnc	$⊢ φ \to \int_{A} (ℜ (C) ℜ (B) - ℑ (C) ℑ (B)) d x = \int_{A} ℜ (C) ℜ (B) d x - \int_{A} ℑ (C) ℑ (B) d x$
134	124	itgeq2dv	$⊢ φ \to \int_{A} ℜ (C B) d x = \int_{A} (ℜ (C) ℜ (B) - ℑ (C) ℑ (B)) d x$
135	111 115	itgneg	$⊢ φ \to - \int_{A} ℑ (C) ℑ (B) d x = \int_{A} (- ℑ (C) ℑ (B)) d x$
136	59 32	mulneg1d	$⊢ (φ \land x \in A) \to (- ℑ (C)) ℑ (B) = - ℑ (C) ℑ (B)$
137	136	itgeq2dv	$⊢ φ \to \int_{A} (- ℑ (C)) ℑ (B) d x = \int_{A} (- ℑ (C) ℑ (B)) d x$
138	135 137	eqtr4d	$⊢ φ \to - \int_{A} ℑ (C) ℑ (B) d x = \int_{A} (- ℑ (C)) ℑ (B) d x$
139	138	oveq2d	$⊢ φ \to \int_{A} ℜ (C) ℜ (B) d x + (- \int_{A} ℑ (C) ℑ (B) d x) = \int_{A} ℜ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x$
140	111 115	itgcl	$⊢ φ \to \int_{A} ℑ (C) ℑ (B) d x \in ℂ$
141	29 140	negsubd	$⊢ φ \to \int_{A} ℜ (C) ℜ (B) d x + (- \int_{A} ℑ (C) ℑ (B) d x) = \int_{A} ℜ (C) ℜ (B) d x - \int_{A} ℑ (C) ℑ (B) d x$
142	139 141	eqtr3d	$⊢ φ \to \int_{A} ℜ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x = \int_{A} ℜ (C) ℜ (B) d x - \int_{A} ℑ (C) ℑ (B) d x$
143	133 134 142	3eqtr4d	$⊢ φ \to \int_{A} ℜ (C B) d x = \int_{A} ℜ (C) ℜ (B) d x + \int_{A} (- ℑ (C)) ℑ (B) d x$
144	116 10	immuld	$⊢ (φ \land x \in A) \to ℑ (C B) = ℜ (C) ℑ (B) + ℑ (C) ℜ (B)$
145	144	itgeq2dv	$⊢ φ \to \int_{A} ℑ (C B) d x = \int_{A} (ℜ (C) ℑ (B) + ℑ (C) ℜ (B)) d x$
146		imf	$⊢ ℑ : ℂ ⟶ ℝ$
147	146	a1i	$⊢ φ \to ℑ : ℂ ⟶ ℝ$
148	147	feqmptd	$⊢ φ \to ℑ = (k \in ℂ ⟼ ℑ (k))$
149		fveq2	$⊢ k = C B \to ℑ (k) = ℑ (C B)$
150	117 118 148 149	fmptco	$⊢ φ \to ℑ \circ (x \in A ⟼ C B) = (x \in A ⟼ ℑ (C B))$
151	144	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℑ (C B)) = (x \in A ⟼ ℜ (C) ℑ (B) + ℑ (C) ℜ (B))$
152	150 151	eqtrd	$⊢ φ \to ℑ \circ (x \in A ⟼ C B) = (x \in A ⟼ ℜ (C) ℑ (B) + ℑ (C) ℜ (B))$
153	130	simprd	$⊢ φ \to ℑ \circ (x \in A ⟼ C B) \in MblFn$
154	152 153	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℜ (C) ℑ (B) + ℑ (C) ℜ (B)) \in MblFn$
155	33 42 60 66 154	itgaddnc	$⊢ φ \to \int_{A} (ℜ (C) ℑ (B) + ℑ (C) ℜ (B)) d x = \int_{A} ℜ (C) ℑ (B) d x + \int_{A} ℑ (C) ℜ (B) d x$
156	145 155	eqtrd	$⊢ φ \to \int_{A} ℑ (C B) d x = \int_{A} ℜ (C) ℑ (B) d x + \int_{A} ℑ (C) ℜ (B) d x$
157	156	oveq2d	$⊢ φ \to i \int_{A} ℑ (C B) d x = i (\int_{A} ℜ (C) ℑ (B) d x + \int_{A} ℑ (C) ℜ (B) d x)$
158	71 43 67	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$
159	157 158	eqtrd	$⊢ φ \to i \int_{A} ℑ (C B) d x = i \int_{A} ℜ (C) ℑ (B) d x + i \int_{A} ℑ (C) ℜ (B) d x$
160	143 159	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$
161	70 110 160	3eqtr4d	$⊢ φ \to (ℜ (C) + i ℑ (C)) \int_{A} B d x = \int_{A} ℜ (C B) d x + i \int_{A} ℑ (C B) d x$
162	1	replimd	$⊢ φ \to C = ℜ (C) + i ℑ (C)$
163	162	oveq1d	$⊢ φ \to C \int_{A} B d x = (ℜ (C) + i ℑ (C)) \int_{A} B d x$
164	1 2 3 4	iblmulc2nc	$⊢ φ \to (x \in A ⟼ C B) \in 𝐿^{1}$
165	117 164	itgcnval	$⊢ φ \to \int_{A} C B d x = \int_{A} ℜ (C B) d x + i \int_{A} ℑ (C B) d x$
166	161 163 165	3eqtr4d	$⊢ φ \to C \int_{A} B d x = \int_{A} C B d x$

Metamath Proof Explorer

Theorem itgmulc2nc

Proof