dvcmul

Description: The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

	Ref	Expression
Hypotheses	dvcmul.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvcmul.f	$⊢ φ \to F : X ⟶ ℂ$
	dvcmul.a	$⊢ φ \to A \in ℂ$
	dvcmul.x	$⊢ φ \to X \subseteq S$
	dvcmul.c	$⊢ φ \to C \in dom F_{S}^{'}$
Assertion	dvcmul	$⊢ φ \to {((S \times \{A\}) \times_{f} F)}_{S}^{'} (C) = A F_{S}^{'} (C)$

Proof

Step	Hyp	Ref	Expression
1		dvcmul.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvcmul.f	$⊢ φ \to F : X ⟶ ℂ$
3		dvcmul.a	$⊢ φ \to A \in ℂ$
4		dvcmul.x	$⊢ φ \to X \subseteq S$
5		dvcmul.c	$⊢ φ \to C \in dom F_{S}^{'}$
6		fconst6g	$⊢ A \in ℂ \to (S \times \{A\}) : S ⟶ ℂ$
7	3 6	syl	$⊢ φ \to (S \times \{A\}) : S ⟶ ℂ$
8		ssidd	$⊢ φ \to S \subseteq S$
9		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
10	1 9	syl	$⊢ φ \to S \subseteq ℂ$
11	10 2 4	dvbss	$⊢ φ \to dom F_{S}^{'} \subseteq X$
12	11 5	sseldd	$⊢ φ \to C \in X$
13	4 12	sseldd	$⊢ φ \to C \in S$
14		fconst6g	$⊢ A \in ℂ \to (ℂ \times \{A\}) : ℂ ⟶ ℂ$
15	3 14	syl	$⊢ φ \to (ℂ \times \{A\}) : ℂ ⟶ ℂ$
16		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
17		dvconst	$⊢ A \in ℂ \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$
18	3 17	syl	$⊢ φ \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$
19	18	dmeqd	$⊢ φ \to dom {(ℂ \times \{A\})}_{ℂ}^{'} = dom (ℂ \times \{0\})$
20		c0ex	$⊢ 0 \in V$
21	20	fconst	$⊢ (ℂ \times \{0\}) : ℂ ⟶ \{0\}$
22	21	fdmi	$⊢ dom (ℂ \times \{0\}) = ℂ$
23	19 22	eqtrdi	$⊢ φ \to dom {(ℂ \times \{A\})}_{ℂ}^{'} = ℂ$
24	10 23	sseqtrrd	$⊢ φ \to S \subseteq dom {(ℂ \times \{A\})}_{ℂ}^{'}$
25		dvres3	$⊢ ((S \in \{ℝ, ℂ\} \land (ℂ \times \{A\}) : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land S \subseteq dom {(ℂ \times \{A\})}_{ℂ}^{'})) \to S D ({(ℂ \times \{A\}) ↾}_{S}) = {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S}$
26	1 15 16 24 25	syl22anc	$⊢ φ \to S D ({(ℂ \times \{A\}) ↾}_{S}) = {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S}$
27		xpssres	$⊢ S \subseteq ℂ \to {(ℂ \times \{A\}) ↾}_{S} = S \times \{A\}$
28	10 27	syl	$⊢ φ \to {(ℂ \times \{A\}) ↾}_{S} = S \times \{A\}$
29	28	oveq2d	$⊢ φ \to S D ({(ℂ \times \{A\}) ↾}_{S}) = S D (S \times \{A\})$
30	18	reseq1d	$⊢ φ \to {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S} = {(ℂ \times \{0\}) ↾}_{S}$
31		xpssres	$⊢ S \subseteq ℂ \to {(ℂ \times \{0\}) ↾}_{S} = S \times \{0\}$
32	10 31	syl	$⊢ φ \to {(ℂ \times \{0\}) ↾}_{S} = S \times \{0\}$
33	30 32	eqtrd	$⊢ φ \to {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S} = S \times \{0\}$
34	26 29 33	3eqtr3d	$⊢ φ \to S D (S \times \{A\}) = S \times \{0\}$
35	20	fconst2	$⊢ {(S \times \{A\})}_{S}^{'} : S ⟶ \{0\} \leftrightarrow S D (S \times \{A\}) = S \times \{0\}$
36	34 35	sylibr	$⊢ φ \to {(S \times \{A\})}_{S}^{'} : S ⟶ \{0\}$
37	36	fdmd	$⊢ φ \to dom {(S \times \{A\})}_{S}^{'} = S$
38	13 37	eleqtrrd	$⊢ φ \to C \in dom {(S \times \{A\})}_{S}^{'}$
39	7 8 2 4 1 38 5	dvmul	$⊢ φ \to {((S \times \{A\}) \times_{f} F)}_{S}^{'} (C) = {(S \times \{A\})}_{S}^{'} (C) F (C) + F_{S}^{'} (C) (S \times \{A\}) (C)$
40	34	fveq1d	$⊢ φ \to {(S \times \{A\})}_{S}^{'} (C) = (S \times \{0\}) (C)$
41	20	fvconst2	$⊢ C \in S \to (S \times \{0\}) (C) = 0$
42	13 41	syl	$⊢ φ \to (S \times \{0\}) (C) = 0$
43	40 42	eqtrd	$⊢ φ \to {(S \times \{A\})}_{S}^{'} (C) = 0$
44	43	oveq1d	$⊢ φ \to {(S \times \{A\})}_{S}^{'} (C) F (C) = 0 \cdot F (C)$
45	2 12	ffvelrnd	$⊢ φ \to F (C) \in ℂ$
46	45	mul02d	$⊢ φ \to 0 \cdot F (C) = 0$
47	44 46	eqtrd	$⊢ φ \to {(S \times \{A\})}_{S}^{'} (C) F (C) = 0$
48		fvconst2g	$⊢ (A \in ℂ \land C \in S) \to (S \times \{A\}) (C) = A$
49	3 13 48	syl2anc	$⊢ φ \to (S \times \{A\}) (C) = A$
50	49	oveq2d	$⊢ φ \to F_{S}^{'} (C) (S \times \{A\}) (C) = F_{S}^{'} (C) A$
51		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
52	1 51	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
53	52 5	ffvelrnd	$⊢ φ \to F_{S}^{'} (C) \in ℂ$
54	53 3	mulcomd	$⊢ φ \to F_{S}^{'} (C) A = A F_{S}^{'} (C)$
55	50 54	eqtrd	$⊢ φ \to F_{S}^{'} (C) (S \times \{A\}) (C) = A F_{S}^{'} (C)$
56	47 55	oveq12d	$⊢ φ \to {(S \times \{A\})}_{S}^{'} (C) F (C) + F_{S}^{'} (C) (S \times \{A\}) (C) = 0 + A F_{S}^{'} (C)$
57	3 53	mulcld	$⊢ φ \to A F_{S}^{'} (C) \in ℂ$
58	57	addid2d	$⊢ φ \to 0 + A F_{S}^{'} (C) = A F_{S}^{'} (C)$
59	39 56 58	3eqtrd	$⊢ φ \to {((S \times \{A\}) \times_{f} F)}_{S}^{'} (C) = A F_{S}^{'} (C)$

Metamath Proof Explorer

Theorem dvcmul

Proof