itg1mulc

Description: The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	i1fmulc.2	$⊢ φ \to F \in dom \int^{1}$
	i1fmulc.3	$⊢ φ \to A \in ℝ$
Assertion	itg1mulc	$⊢ φ \to \int^{1} ((ℝ \times \{A\}) \times_{f} F) = A \int^{1} (F)$

Proof

Step	Hyp	Ref	Expression
1		i1fmulc.2	$⊢ φ \to F \in dom \int^{1}$
2		i1fmulc.3	$⊢ φ \to A \in ℝ$
3		itg10	$⊢ \int^{1} (ℝ \times \{0\}) = 0$
4		reex	$⊢ ℝ \in V$
5	4	a1i	$⊢ (φ \land A = 0) \to ℝ \in V$
6		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
7	1 6	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
8	7	adantr	$⊢ (φ \land A = 0) \to F : ℝ ⟶ ℝ$
9	2	adantr	$⊢ (φ \land A = 0) \to A \in ℝ$
10		0red	$⊢ (φ \land A = 0) \to 0 \in ℝ$
11		simplr	$⊢ ((φ \land A = 0) \land x \in ℝ) \to A = 0$
12	11	oveq1d	$⊢ ((φ \land A = 0) \land x \in ℝ) \to A x = 0 \cdot x$
13		mul02lem2	$⊢ x \in ℝ \to 0 \cdot x = 0$
14	13	adantl	$⊢ ((φ \land A = 0) \land x \in ℝ) \to 0 \cdot x = 0$
15	12 14	eqtrd	$⊢ ((φ \land A = 0) \land x \in ℝ) \to A x = 0$
16	5 8 9 10 15	caofid2	$⊢ (φ \land A = 0) \to (ℝ \times \{A\}) \times_{f} F = ℝ \times \{0\}$
17	16	fveq2d	$⊢ (φ \land A = 0) \to \int^{1} ((ℝ \times \{A\}) \times_{f} F) = \int^{1} (ℝ \times \{0\})$
18		simpr	$⊢ (φ \land A = 0) \to A = 0$
19	18	oveq1d	$⊢ (φ \land A = 0) \to A \int^{1} (F) = 0 \cdot \int^{1} (F)$
20		itg1cl	$⊢ F \in dom \int^{1} \to \int^{1} (F) \in ℝ$
21	1 20	syl	$⊢ φ \to \int^{1} (F) \in ℝ$
22	21	recnd	$⊢ φ \to \int^{1} (F) \in ℂ$
23	22	mul02d	$⊢ φ \to 0 \cdot \int^{1} (F) = 0$
24	23	adantr	$⊢ (φ \land A = 0) \to 0 \cdot \int^{1} (F) = 0$
25	19 24	eqtrd	$⊢ (φ \land A = 0) \to A \int^{1} (F) = 0$
26	3 17 25	3eqtr4a	$⊢ (φ \land A = 0) \to \int^{1} ((ℝ \times \{A\}) \times_{f} F) = A \int^{1} (F)$
27	1 2	i1fmulc	$⊢ φ \to (ℝ \times \{A\}) \times_{f} F \in dom \int^{1}$
28	27	adantr	$⊢ (φ \land A \neq 0) \to (ℝ \times \{A\}) \times_{f} F \in dom \int^{1}$
29		i1ff	$⊢ (ℝ \times \{A\}) \times_{f} F \in dom \int^{1} \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ ℝ$
30	28 29	syl	$⊢ (φ \land A \neq 0) \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ ℝ$
31	30	frnd	$⊢ (φ \land A \neq 0) \to ran ((ℝ \times \{A\}) \times_{f} F) \subseteq ℝ$
32	31	ssdifssd	$⊢ (φ \land A \neq 0) \to ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \subseteq ℝ$
33	32	sselda	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to m \in ℝ$
34	33	recnd	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to m \in ℂ$
35	2	adantr	$⊢ (φ \land A \neq 0) \to A \in ℝ$
36	35	recnd	$⊢ (φ \land A \neq 0) \to A \in ℂ$
37	36	adantr	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \in ℂ$
38		simplr	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \neq 0$
39	34 37 38	divcan2d	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A (\frac{m}{A}) = m$
40	1 2	i1fmulclem	$⊢ ((φ \land A \neq 0) \land m \in ℝ) \to {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}] = F^{-1} [\{\frac{m}{A}\}]$
41	33 40	syldan	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}] = F^{-1} [\{\frac{m}{A}\}]$
42	41	fveq2d	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}]) = vol (F^{-1} [\{\frac{m}{A}\}])$
43	42	eqcomd	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to vol (F^{-1} [\{\frac{m}{A}\}]) = vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}])$
44	39 43	oveq12d	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}]) = m vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}])$
45	2	ad2antrr	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \in ℝ$
46	33 45 38	redivcld	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{m}{A} \in ℝ$
47	46	recnd	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{m}{A} \in ℂ$
48	1	ad2antrr	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to F \in dom \int^{1}$
49	45	recnd	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \in ℂ$
50		eldifsni	$⊢ m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \to m \neq 0$
51	50	adantl	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to m \neq 0$
52	34 49 51 38	divne0d	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{m}{A} \neq 0$
53		eldifsn	$⊢ \frac{m}{A} \in (ℝ ∖ \{0\}) \leftrightarrow (\frac{m}{A} \in ℝ \land \frac{m}{A} \neq 0)$
54	46 52 53	sylanbrc	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{m}{A} \in (ℝ ∖ \{0\})$
55		i1fima2sn	$⊢ (F \in dom \int^{1} \land \frac{m}{A} \in (ℝ ∖ \{0\})) \to vol (F^{-1} [\{\frac{m}{A}\}]) \in ℝ$
56	48 54 55	syl2anc	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to vol (F^{-1} [\{\frac{m}{A}\}]) \in ℝ$
57	56	recnd	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to vol (F^{-1} [\{\frac{m}{A}\}]) \in ℂ$
58	37 47 57	mulassd	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}]) = A (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
59	44 58	eqtr3d	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to m vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}]) = A (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
60	59	sumeq2dv	$⊢ (φ \land A \neq 0) \to \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} m vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}]) = \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} A (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
61		i1frn	$⊢ (ℝ \times \{A\}) \times_{f} F \in dom \int^{1} \to ran ((ℝ \times \{A\}) \times_{f} F) \in Fin$
62	28 61	syl	$⊢ (φ \land A \neq 0) \to ran ((ℝ \times \{A\}) \times_{f} F) \in Fin$
63		difss	$⊢ ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \subseteq ran ((ℝ \times \{A\}) \times_{f} F)$
64		ssfi	$⊢ (ran ((ℝ \times \{A\}) \times_{f} F) \in Fin \land ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \subseteq ran ((ℝ \times \{A\}) \times_{f} F)) \to ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \in Fin$
65	62 63 64	sylancl	$⊢ (φ \land A \neq 0) \to ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \in Fin$
66	47 57	mulcld	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}]) \in ℂ$
67	65 36 66	fsummulc2	$⊢ (φ \land A \neq 0) \to A \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}]) = \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} A (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
68	60 67	eqtr4d	$⊢ (φ \land A \neq 0) \to \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} m vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}]) = A \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
69		itg1val	$⊢ (ℝ \times \{A\}) \times_{f} F \in dom \int^{1} \to \int^{1} ((ℝ \times \{A\}) \times_{f} F) = \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} m vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}])$
70	28 69	syl	$⊢ (φ \land A \neq 0) \to \int^{1} ((ℝ \times \{A\}) \times_{f} F) = \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} m vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{m\}])$
71	1	adantr	$⊢ (φ \land A \neq 0) \to F \in dom \int^{1}$
72		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
73	71 72	syl	$⊢ (φ \land A \neq 0) \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
74		id	$⊢ k = \frac{m}{A} \to k = \frac{m}{A}$
75		sneq	$⊢ k = \frac{m}{A} \to \{k\} = \{\frac{m}{A}\}$
76	75	imaeq2d	$⊢ k = \frac{m}{A} \to F^{-1} [\{k\}] = F^{-1} [\{\frac{m}{A}\}]$
77	76	fveq2d	$⊢ k = \frac{m}{A} \to vol (F^{-1} [\{k\}]) = vol (F^{-1} [\{\frac{m}{A}\}])$
78	74 77	oveq12d	$⊢ k = \frac{m}{A} \to k vol (F^{-1} [\{k\}]) = (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
79		eqid	$⊢ (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) ⟼ \frac{n}{A}) = (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) ⟼ \frac{n}{A})$
80		eldifi	$⊢ n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \to n \in ran ((ℝ \times \{A\}) \times_{f} F)$
81	4	a1i	$⊢ φ \to ℝ \in V$
82	7	ffnd	$⊢ φ \to F Fn ℝ$
83		eqidd	$⊢ (φ \land y \in ℝ) \to F (y) = F (y)$
84	81 2 82 83	ofc1	$⊢ (φ \land y \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) (y) = A F (y)$
85	84	adantlr	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) (y) = A F (y)$
86	85	oveq1d	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A} = \frac{A F (y)}{A}$
87	7	adantr	$⊢ (φ \land A \neq 0) \to F : ℝ ⟶ ℝ$
88	87	ffvelcdmda	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to F (y) \in ℝ$
89	88	recnd	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to F (y) \in ℂ$
90	36	adantr	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to A \in ℂ$
91		simplr	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to A \neq 0$
92	89 90 91	divcan3d	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to \frac{A F (y)}{A} = F (y)$
93	86 92	eqtrd	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A} = F (y)$
94	87	ffnd	$⊢ (φ \land A \neq 0) \to F Fn ℝ$
95		fnfvelrn	$⊢ (F Fn ℝ \land y \in ℝ) \to F (y) \in ran F$
96	94 95	sylan	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to F (y) \in ran F$
97	93 96	eqeltrd	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A} \in ran F$
98	97	ralrimiva	$⊢ (φ \land A \neq 0) \to \forall y \in ℝ \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A} \in ran F$
99	30	ffnd	$⊢ (φ \land A \neq 0) \to ((ℝ \times \{A\}) \times_{f} F) Fn ℝ$
100		oveq1	$⊢ n = ((ℝ \times \{A\}) \times_{f} F) (y) \to \frac{n}{A} = \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A}$
101	100	eleq1d	$⊢ n = ((ℝ \times \{A\}) \times_{f} F) (y) \to (\frac{n}{A} \in ran F \leftrightarrow \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A} \in ran F)$
102	101	ralrn	$⊢ ((ℝ \times \{A\}) \times_{f} F) Fn ℝ \to (\forall n \in ran ((ℝ \times \{A\}) \times_{f} F) \frac{n}{A} \in ran F \leftrightarrow \forall y \in ℝ \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A} \in ran F)$
103	99 102	syl	$⊢ (φ \land A \neq 0) \to (\forall n \in ran ((ℝ \times \{A\}) \times_{f} F) \frac{n}{A} \in ran F \leftrightarrow \forall y \in ℝ \frac{((ℝ \times \{A\}) \times_{f} F) (y)}{A} \in ran F)$
104	98 103	mpbird	$⊢ (φ \land A \neq 0) \to \forall n \in ran ((ℝ \times \{A\}) \times_{f} F) \frac{n}{A} \in ran F$
105	104	r19.21bi	$⊢ ((φ \land A \neq 0) \land n \in ran ((ℝ \times \{A\}) \times_{f} F)) \to \frac{n}{A} \in ran F$
106	80 105	sylan2	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{n}{A} \in ran F$
107	32	sselda	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to n \in ℝ$
108	107	recnd	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to n \in ℂ$
109	36	adantr	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \in ℂ$
110		eldifsni	$⊢ n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \to n \neq 0$
111	110	adantl	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to n \neq 0$
112		simplr	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \neq 0$
113	108 109 111 112	divne0d	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{n}{A} \neq 0$
114		eldifsn	$⊢ \frac{n}{A} \in (ran F ∖ \{0\}) \leftrightarrow (\frac{n}{A} \in ran F \land \frac{n}{A} \neq 0)$
115	106 113 114	sylanbrc	$⊢ ((φ \land A \neq 0) \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{n}{A} \in (ran F ∖ \{0\})$
116		eldifi	$⊢ k \in (ran F ∖ \{0\}) \to k \in ran F$
117		fnfvelrn	$⊢ (((ℝ \times \{A\}) \times_{f} F) Fn ℝ \land y \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) (y) \in ran ((ℝ \times \{A\}) \times_{f} F)$
118	99 117	sylan	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) (y) \in ran ((ℝ \times \{A\}) \times_{f} F)$
119	85 118	eqeltrrd	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to A F (y) \in ran ((ℝ \times \{A\}) \times_{f} F)$
120	119	ralrimiva	$⊢ (φ \land A \neq 0) \to \forall y \in ℝ A F (y) \in ran ((ℝ \times \{A\}) \times_{f} F)$
121		oveq2	$⊢ k = F (y) \to A k = A F (y)$
122	121	eleq1d	$⊢ k = F (y) \to (A k \in ran ((ℝ \times \{A\}) \times_{f} F) \leftrightarrow A F (y) \in ran ((ℝ \times \{A\}) \times_{f} F))$
123	122	ralrn	$⊢ F Fn ℝ \to (\forall k \in ran F A k \in ran ((ℝ \times \{A\}) \times_{f} F) \leftrightarrow \forall y \in ℝ A F (y) \in ran ((ℝ \times \{A\}) \times_{f} F))$
124	94 123	syl	$⊢ (φ \land A \neq 0) \to (\forall k \in ran F A k \in ran ((ℝ \times \{A\}) \times_{f} F) \leftrightarrow \forall y \in ℝ A F (y) \in ran ((ℝ \times \{A\}) \times_{f} F))$
125	120 124	mpbird	$⊢ (φ \land A \neq 0) \to \forall k \in ran F A k \in ran ((ℝ \times \{A\}) \times_{f} F)$
126	125	r19.21bi	$⊢ ((φ \land A \neq 0) \land k \in ran F) \to A k \in ran ((ℝ \times \{A\}) \times_{f} F)$
127	116 126	sylan2	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to A k \in ran ((ℝ \times \{A\}) \times_{f} F)$
128	36	adantr	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to A \in ℂ$
129	87	frnd	$⊢ (φ \land A \neq 0) \to ran F \subseteq ℝ$
130	129	ssdifssd	$⊢ (φ \land A \neq 0) \to ran F ∖ \{0\} \subseteq ℝ$
131	130	sselda	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to k \in ℝ$
132	131	recnd	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to k \in ℂ$
133		simplr	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to A \neq 0$
134		eldifsni	$⊢ k \in (ran F ∖ \{0\}) \to k \neq 0$
135	134	adantl	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to k \neq 0$
136	128 132 133 135	mulne0d	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to A k \neq 0$
137		eldifsn	$⊢ A k \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \leftrightarrow (A k \in ran ((ℝ \times \{A\}) \times_{f} F) \land A k \neq 0)$
138	127 136 137	sylanbrc	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to A k \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})$
139		simpl	$⊢ (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\})) \to n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})$
140		ssel2	$⊢ (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \subseteq ℝ \land n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to n \in ℝ$
141	32 139 140	syl2an	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to n \in ℝ$
142	141	recnd	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to n \in ℂ$
143	2	ad2antrr	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to A \in ℝ$
144	143	recnd	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to A \in ℂ$
145	131	adantrl	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to k \in ℝ$
146	145	recnd	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to k \in ℂ$
147		simplr	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to A \neq 0$
148	142 144 146 147	divmuld	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to (\frac{n}{A} = k \leftrightarrow A k = n)$
149	148	bicomd	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to (A k = n \leftrightarrow \frac{n}{A} = k)$
150		eqcom	$⊢ n = A k \leftrightarrow A k = n$
151		eqcom	$⊢ k = \frac{n}{A} \leftrightarrow \frac{n}{A} = k$
152	149 150 151	3bitr4g	$⊢ ((φ \land A \neq 0) \land (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \land k \in (ran F ∖ \{0\}))) \to (n = A k \leftrightarrow k = \frac{n}{A})$
153	79 115 138 152	f1o2d	$⊢ (φ \land A \neq 0) \to (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) ⟼ \frac{n}{A}) : ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \underset{1-1 onto}{⟶} ran F ∖ \{0\}$
154		oveq1	$⊢ n = m \to \frac{n}{A} = \frac{m}{A}$
155		ovex	$⊢ \frac{m}{A} \in V$
156	154 79 155	fvmpt	$⊢ m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \to (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) ⟼ \frac{n}{A}) (m) = \frac{m}{A}$
157	156	adantl	$⊢ ((φ \land A \neq 0) \land m \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to (n \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) ⟼ \frac{n}{A}) (m) = \frac{m}{A}$
158		i1fima2sn	$⊢ (F \in dom \int^{1} \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) \in ℝ$
159	71 158	sylan	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) \in ℝ$
160	131 159	remulcld	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to k vol (F^{-1} [\{k\}]) \in ℝ$
161	160	recnd	$⊢ ((φ \land A \neq 0) \land k \in (ran F ∖ \{0\})) \to k vol (F^{-1} [\{k\}]) \in ℂ$
162	78 65 153 157 161	fsumf1o	$⊢ (φ \land A \neq 0) \to \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}]) = \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
163	73 162	eqtrd	$⊢ (φ \land A \neq 0) \to \int^{1} (F) = \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
164	163	oveq2d	$⊢ (φ \land A \neq 0) \to A \int^{1} (F) = A \sum_{m \in ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}} (\frac{m}{A}) vol (F^{-1} [\{\frac{m}{A}\}])$
165	68 70 164	3eqtr4d	$⊢ (φ \land A \neq 0) \to \int^{1} ((ℝ \times \{A\}) \times_{f} F) = A \int^{1} (F)$
166	26 165	pm2.61dane	$⊢ φ \to \int^{1} ((ℝ \times \{A\}) \times_{f} F) = A \int^{1} (F)$

Metamath Proof Explorer

Theorem itg1mulc

Proof