mbfmullem2

	Ref	Expression
Hypotheses	mbfmul.1	$⊢ φ \to F \in MblFn$
	mbfmul.2	$⊢ φ \to G \in MblFn$
	mbfmul.3	$⊢ φ \to F : A ⟶ ℝ$
	mbfmul.4	$⊢ φ \to G : A ⟶ ℝ$
	mbfmul.5	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
	mbfmul.6	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
	mbfmul.7	$⊢ φ \to Q : ℕ ⟶ dom \int^{1}$
	mbfmul.8	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ Q (n) (x)) ⇝ G (x)$
Assertion	mbfmullem2	$⊢ φ \to F \times_{f} G \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfmul.1	$⊢ φ \to F \in MblFn$
2		mbfmul.2	$⊢ φ \to G \in MblFn$
3		mbfmul.3	$⊢ φ \to F : A ⟶ ℝ$
4		mbfmul.4	$⊢ φ \to G : A ⟶ ℝ$
5		mbfmul.5	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
6		mbfmul.6	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
7		mbfmul.7	$⊢ φ \to Q : ℕ ⟶ dom \int^{1}$
8		mbfmul.8	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ Q (n) (x)) ⇝ G (x)$
9	3	ffnd	$⊢ φ \to F Fn A$
10	4	ffnd	$⊢ φ \to G Fn A$
11	3	fdmd	$⊢ φ \to dom F = A$
12		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
13	1 12	syl	$⊢ φ \to dom F \in dom vol$
14	11 13	eqeltrrd	$⊢ φ \to A \in dom vol$
15		inidm	$⊢ A \cap A = A$
16		eqidd	$⊢ (φ \land x \in A) \to F (x) = F (x)$
17		eqidd	$⊢ (φ \land x \in A) \to G (x) = G (x)$
18	9 10 14 14 15 16 17	offval	$⊢ φ \to F \times_{f} G = (x \in A ⟼ F (x) G (x))$
19		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
20		1zzd	$⊢ φ \to 1 \in ℤ$
21		1zzd	$⊢ (φ \land x \in A) \to 1 \in ℤ$
22		nnex	$⊢ ℕ \in V$
23	22	mptex	$⊢ (n \in ℕ ⟼ P (n) (x) Q (n) (x)) \in V$
24	23	a1i	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ P (n) (x) Q (n) (x)) \in V$
25	5	ffvelrnda	$⊢ (φ \land n \in ℕ) \to P (n) \in dom \int^{1}$
26		i1ff	$⊢ P (n) \in dom \int^{1} \to P (n) : ℝ ⟶ ℝ$
27	25 26	syl	$⊢ (φ \land n \in ℕ) \to P (n) : ℝ ⟶ ℝ$
28	27	adantlr	$⊢ ((φ \land x \in A) \land n \in ℕ) \to P (n) : ℝ ⟶ ℝ$
29		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
30	14 29	syl	$⊢ φ \to A \subseteq ℝ$
31	30	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
32	31	adantr	$⊢ ((φ \land x \in A) \land n \in ℕ) \to x \in ℝ$
33	28 32	ffvelrnd	$⊢ ((φ \land x \in A) \land n \in ℕ) \to P (n) (x) \in ℝ$
34	33	recnd	$⊢ ((φ \land x \in A) \land n \in ℕ) \to P (n) (x) \in ℂ$
35	34	fmpttd	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ P (n) (x)) : ℕ ⟶ ℂ$
36	35	ffvelrnda	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (x)) (k) \in ℂ$
37	7	ffvelrnda	$⊢ (φ \land n \in ℕ) \to Q (n) \in dom \int^{1}$
38		i1ff	$⊢ Q (n) \in dom \int^{1} \to Q (n) : ℝ ⟶ ℝ$
39	37 38	syl	$⊢ (φ \land n \in ℕ) \to Q (n) : ℝ ⟶ ℝ$
40	39	adantlr	$⊢ ((φ \land x \in A) \land n \in ℕ) \to Q (n) : ℝ ⟶ ℝ$
41	40 32	ffvelrnd	$⊢ ((φ \land x \in A) \land n \in ℕ) \to Q (n) (x) \in ℝ$
42	41	recnd	$⊢ ((φ \land x \in A) \land n \in ℕ) \to Q (n) (x) \in ℂ$
43	42	fmpttd	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ Q (n) (x)) : ℕ ⟶ ℂ$
44	43	ffvelrnda	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (n \in ℕ ⟼ Q (n) (x)) (k) \in ℂ$
45		fveq2	$⊢ n = k \to P (n) = P (k)$
46	45	fveq1d	$⊢ n = k \to P (n) (x) = P (k) (x)$
47		fveq2	$⊢ n = k \to Q (n) = Q (k)$
48	47	fveq1d	$⊢ n = k \to Q (n) (x) = Q (k) (x)$
49	46 48	oveq12d	$⊢ n = k \to P (n) (x) Q (n) (x) = P (k) (x) Q (k) (x)$
50		eqid	$⊢ (n \in ℕ ⟼ P (n) (x) Q (n) (x)) = (n \in ℕ ⟼ P (n) (x) Q (n) (x))$
51		ovex	$⊢ P (k) (x) Q (k) (x) \in V$
52	49 50 51	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ P (n) (x) Q (n) (x)) (k) = P (k) (x) Q (k) (x)$
53	52	adantl	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (x) Q (n) (x)) (k) = P (k) (x) Q (k) (x)$
54		eqid	$⊢ (n \in ℕ ⟼ P (n) (x)) = (n \in ℕ ⟼ P (n) (x))$
55		fvex	$⊢ P (k) (x) \in V$
56	46 54 55	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ P (n) (x)) (k) = P (k) (x)$
57		eqid	$⊢ (n \in ℕ ⟼ Q (n) (x)) = (n \in ℕ ⟼ Q (n) (x))$
58		fvex	$⊢ Q (k) (x) \in V$
59	48 57 58	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ Q (n) (x)) (k) = Q (k) (x)$
60	56 59	oveq12d	$⊢ k \in ℕ \to (n \in ℕ ⟼ P (n) (x)) (k) (n \in ℕ ⟼ Q (n) (x)) (k) = P (k) (x) Q (k) (x)$
61	60	adantl	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (x)) (k) (n \in ℕ ⟼ Q (n) (x)) (k) = P (k) (x) Q (k) (x)$
62	53 61	eqtr4d	$⊢ ((φ \land x \in A) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (x) Q (n) (x)) (k) = (n \in ℕ ⟼ P (n) (x)) (k) (n \in ℕ ⟼ Q (n) (x)) (k)$
63	19 21 6 24 8 36 44 62	climmul	$⊢ (φ \land x \in A) \to (n \in ℕ ⟼ P (n) (x) Q (n) (x)) ⇝ F (x) G (x)$
64	30	adantr	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
65	64	resmptd	$⊢ (φ \land n \in ℕ) \to {(x \in ℝ ⟼ P (n) (x) Q (n) (x)) ↾}_{A} = (x \in A ⟼ P (n) (x) Q (n) (x))$
66	27	ffnd	$⊢ (φ \land n \in ℕ) \to P (n) Fn ℝ$
67	39	ffnd	$⊢ (φ \land n \in ℕ) \to Q (n) Fn ℝ$
68		reex	$⊢ ℝ \in V$
69	68	a1i	$⊢ (φ \land n \in ℕ) \to ℝ \in V$
70		inidm	$⊢ ℝ \cap ℝ = ℝ$
71		eqidd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to P (n) (x) = P (n) (x)$
72		eqidd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to Q (n) (x) = Q (n) (x)$
73	66 67 69 69 70 71 72	offval	$⊢ (φ \land n \in ℕ) \to P (n) \times_{f} Q (n) = (x \in ℝ ⟼ P (n) (x) Q (n) (x))$
74	25 37	i1fmul	$⊢ (φ \land n \in ℕ) \to P (n) \times_{f} Q (n) \in dom \int^{1}$
75		i1fmbf	$⊢ P (n) \times_{f} Q (n) \in dom \int^{1} \to P (n) \times_{f} Q (n) \in MblFn$
76	74 75	syl	$⊢ (φ \land n \in ℕ) \to P (n) \times_{f} Q (n) \in MblFn$
77	73 76	eqeltrrd	$⊢ (φ \land n \in ℕ) \to (x \in ℝ ⟼ P (n) (x) Q (n) (x)) \in MblFn$
78	14	adantr	$⊢ (φ \land n \in ℕ) \to A \in dom vol$
79		mbfres	$⊢ ((x \in ℝ ⟼ P (n) (x) Q (n) (x)) \in MblFn \land A \in dom vol) \to {(x \in ℝ ⟼ P (n) (x) Q (n) (x)) ↾}_{A} \in MblFn$
80	77 78 79	syl2anc	$⊢ (φ \land n \in ℕ) \to {(x \in ℝ ⟼ P (n) (x) Q (n) (x)) ↾}_{A} \in MblFn$
81	65 80	eqeltrrd	$⊢ (φ \land n \in ℕ) \to (x \in A ⟼ P (n) (x) Q (n) (x)) \in MblFn$
82		ovex	$⊢ P (n) (x) Q (n) (x) \in V$
83	82	a1i	$⊢ (φ \land (n \in ℕ \land x \in A)) \to P (n) (x) Q (n) (x) \in V$
84	19 20 63 81 83	mbflim	$⊢ φ \to (x \in A ⟼ F (x) G (x)) \in MblFn$
85	18 84	eqeltrd	$⊢ φ \to F \times_{f} G \in MblFn$

Metamath Proof Explorer

Theorem mbfmullem2

Proof