dvcmulf

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 ℂ$
	dvcmulf.df	$⊢ φ \to dom F_{S}^{'} = X$
Assertion	dvcmulf	$⊢ φ \to S D ((S \times \{A\}) \times_{f} F) = (S \times \{A\}) \times_{f} F_{S}^{'}$

Proof

Step	Hyp	Ref	Expression
1		dvcmul.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvcmul.f	$⊢ φ \to F : X ⟶ ℂ$
3		dvcmul.a	$⊢ φ \to A \in ℂ$
4		dvcmulf.df	$⊢ φ \to dom F_{S}^{'} = X$
5		fconstg	$⊢ A \in ℂ \to (X \times \{A\}) : X ⟶ \{A\}$
6	3 5	syl	$⊢ φ \to (X \times \{A\}) : X ⟶ \{A\}$
7	3	snssd	$⊢ φ \to \{A\} \subseteq ℂ$
8	6 7	fssd	$⊢ φ \to (X \times \{A\}) : X ⟶ ℂ$
9		c0ex	$⊢ 0 \in V$
10	9	fconst	$⊢ (X \times \{0\}) : X ⟶ \{0\}$
11		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
12	1 11	syl	$⊢ φ \to S \subseteq ℂ$
13		fconstg	$⊢ A \in ℂ \to (S \times \{A\}) : S ⟶ \{A\}$
14	3 13	syl	$⊢ φ \to (S \times \{A\}) : S ⟶ \{A\}$
15	14 7	fssd	$⊢ φ \to (S \times \{A\}) : S ⟶ ℂ$
16		ssidd	$⊢ φ \to S \subseteq S$
17		dvbsss	$⊢ dom F_{S}^{'} \subseteq S$
18	17	a1i	$⊢ φ \to dom F_{S}^{'} \subseteq S$
19	4 18	eqsstrrd	$⊢ φ \to X \subseteq S$
20		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
21		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
22	20 21	dvres	$⊢ ((S \subseteq ℂ \land (S \times \{A\}) : S ⟶ ℂ) \land (S \subseteq S \land X \subseteq S)) \to S D ({(S \times \{A\}) ↾}_{X}) = {{(S \times \{A\})}_{S}^{'} ↾}_{int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)}$
23	12 15 16 19 22	syl22anc	$⊢ φ \to S D ({(S \times \{A\}) ↾}_{X}) = {{(S \times \{A\})}_{S}^{'} ↾}_{int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)}$
24	19	resmptd	$⊢ φ \to {(x \in S ⟼ A) ↾}_{X} = (x \in X ⟼ A)$
25		fconstmpt	$⊢ S \times \{A\} = (x \in S ⟼ A)$
26	25	reseq1i	$⊢ {(S \times \{A\}) ↾}_{X} = {(x \in S ⟼ A) ↾}_{X}$
27		fconstmpt	$⊢ X \times \{A\} = (x \in X ⟼ A)$
28	24 26 27	3eqtr4g	$⊢ φ \to {(S \times \{A\}) ↾}_{X} = X \times \{A\}$
29	28	oveq2d	$⊢ φ \to S D ({(S \times \{A\}) ↾}_{X}) = S D (X \times \{A\})$
30	19	resmptd	$⊢ φ \to {(x \in S ⟼ 0) ↾}_{X} = (x \in X ⟼ 0)$
31		fconstg	$⊢ A \in ℂ \to (ℂ \times \{A\}) : ℂ ⟶ \{A\}$
32	3 31	syl	$⊢ φ \to (ℂ \times \{A\}) : ℂ ⟶ \{A\}$
33	32 7	fssd	$⊢ φ \to (ℂ \times \{A\}) : ℂ ⟶ ℂ$
34		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
35		dvconst	$⊢ A \in ℂ \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$
36	3 35	syl	$⊢ φ \to ℂ D (ℂ \times \{A\}) = ℂ \times \{0\}$
37	36	dmeqd	$⊢ φ \to dom {(ℂ \times \{A\})}_{ℂ}^{'} = dom (ℂ \times \{0\})$
38	9	fconst	$⊢ (ℂ \times \{0\}) : ℂ ⟶ \{0\}$
39	38	fdmi	$⊢ dom (ℂ \times \{0\}) = ℂ$
40	37 39	eqtrdi	$⊢ φ \to dom {(ℂ \times \{A\})}_{ℂ}^{'} = ℂ$
41	12 40	sseqtrrd	$⊢ φ \to S \subseteq dom {(ℂ \times \{A\})}_{ℂ}^{'}$
42		dvres3	$⊢ ((S \in \{ℝ, ℂ\} \land (ℂ \times \{A\}) : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land S \subseteq dom {(ℂ \times \{A\})}_{ℂ}^{'})) \to S D ({(ℂ \times \{A\}) ↾}_{S}) = {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S}$
43	1 33 34 41 42	syl22anc	$⊢ φ \to S D ({(ℂ \times \{A\}) ↾}_{S}) = {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S}$
44		xpssres	$⊢ S \subseteq ℂ \to {(ℂ \times \{A\}) ↾}_{S} = S \times \{A\}$
45	12 44	syl	$⊢ φ \to {(ℂ \times \{A\}) ↾}_{S} = S \times \{A\}$
46	45	oveq2d	$⊢ φ \to S D ({(ℂ \times \{A\}) ↾}_{S}) = S D (S \times \{A\})$
47	36	reseq1d	$⊢ φ \to {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S} = {(ℂ \times \{0\}) ↾}_{S}$
48		xpssres	$⊢ S \subseteq ℂ \to {(ℂ \times \{0\}) ↾}_{S} = S \times \{0\}$
49	12 48	syl	$⊢ φ \to {(ℂ \times \{0\}) ↾}_{S} = S \times \{0\}$
50	47 49	eqtrd	$⊢ φ \to {{(ℂ \times \{A\})}_{ℂ}^{'} ↾}_{S} = S \times \{0\}$
51	43 46 50	3eqtr3d	$⊢ φ \to S D (S \times \{A\}) = S \times \{0\}$
52		fconstmpt	$⊢ S \times \{0\} = (x \in S ⟼ 0)$
53	51 52	eqtrdi	$⊢ φ \to S D (S \times \{A\}) = (x \in S ⟼ 0)$
54	20	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
55		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land S \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
56	54 12 55	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
57		topontop	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
58	56 57	syl	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
59		toponuni	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
60	56 59	syl	$⊢ φ \to S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
61	19 60	sseqtrd	$⊢ φ \to X \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
62		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
63	62	ntrss2	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top \land X \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \subseteq X$
64	58 61 63	syl2anc	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \subseteq X$
65	12 2 19 21 20	dvbssntr	$⊢ φ \to dom F_{S}^{'} \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)$
66	4 65	eqsstrrd	$⊢ φ \to X \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)$
67	64 66	eqssd	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) = X$
68	53 67	reseq12d	$⊢ φ \to {{(S \times \{A\})}_{S}^{'} ↾}_{int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)} = {(x \in S ⟼ 0) ↾}_{X}$
69		fconstmpt	$⊢ X \times \{0\} = (x \in X ⟼ 0)$
70	69	a1i	$⊢ φ \to X \times \{0\} = (x \in X ⟼ 0)$
71	30 68 70	3eqtr4d	$⊢ φ \to {{(S \times \{A\})}_{S}^{'} ↾}_{int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)} = X \times \{0\}$
72	23 29 71	3eqtr3d	$⊢ φ \to S D (X \times \{A\}) = X \times \{0\}$
73	72	feq1d	$⊢ φ \to ({(X \times \{A\})}_{S}^{'} : X ⟶ \{0\} \leftrightarrow (X \times \{0\}) : X ⟶ \{0\})$
74	10 73	mpbiri	$⊢ φ \to {(X \times \{A\})}_{S}^{'} : X ⟶ \{0\}$
75	74	fdmd	$⊢ φ \to dom {(X \times \{A\})}_{S}^{'} = X$
76	1 8 2 75 4	dvmulf	$⊢ φ \to S D ((X \times \{A\}) \times_{f} F) = ({(X \times \{A\})}_{S}^{'} \times_{f} F) +_{f} (F_{S}^{'} \times_{f} (X \times \{A\}))$
77		sseqin2	$⊢ X \subseteq S \leftrightarrow S \cap X = X$
78	19 77	sylib	$⊢ φ \to S \cap X = X$
79	78	mpteq1d	$⊢ φ \to (x \in (S \cap X) ⟼ A F (x)) = (x \in X ⟼ A F (x))$
80	14	ffnd	$⊢ φ \to (S \times \{A\}) Fn S$
81	2	ffnd	$⊢ φ \to F Fn X$
82	1 19	ssexd	$⊢ φ \to X \in V$
83		eqid	$⊢ S \cap X = S \cap X$
84		fvconst2g	$⊢ (A \in ℂ \land x \in S) \to (S \times \{A\}) (x) = A$
85	3 84	sylan	$⊢ (φ \land x \in S) \to (S \times \{A\}) (x) = A$
86		eqidd	$⊢ (φ \land x \in X) \to F (x) = F (x)$
87	80 81 1 82 83 85 86	offval	$⊢ φ \to (S \times \{A\}) \times_{f} F = (x \in (S \cap X) ⟼ A F (x))$
88	6	ffnd	$⊢ φ \to (X \times \{A\}) Fn X$
89		inidm	$⊢ X \cap X = X$
90		fvconst2g	$⊢ (A \in ℂ \land x \in X) \to (X \times \{A\}) (x) = A$
91	3 90	sylan	$⊢ (φ \land x \in X) \to (X \times \{A\}) (x) = A$
92	88 81 82 82 89 91 86	offval	$⊢ φ \to (X \times \{A\}) \times_{f} F = (x \in X ⟼ A F (x))$
93	79 87 92	3eqtr4d	$⊢ φ \to (S \times \{A\}) \times_{f} F = (X \times \{A\}) \times_{f} F$
94	93	oveq2d	$⊢ φ \to S D ((S \times \{A\}) \times_{f} F) = S D ((X \times \{A\}) \times_{f} F)$
95	78	mpteq1d	$⊢ φ \to (x \in (S \cap X) ⟼ A F_{S}^{'} (x)) = (x \in X ⟼ A F_{S}^{'} (x))$
96		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
97	1 96	syl	$⊢ φ \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
98	4	feq2d	$⊢ φ \to (F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \leftrightarrow F_{S}^{'} : X ⟶ ℂ)$
99	97 98	mpbid	$⊢ φ \to F_{S}^{'} : X ⟶ ℂ$
100	99	ffnd	$⊢ φ \to F_{S}^{'} Fn X$
101		eqidd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) = F_{S}^{'} (x)$
102	80 100 1 82 83 85 101	offval	$⊢ φ \to (S \times \{A\}) \times_{f} F_{S}^{'} = (x \in (S \cap X) ⟼ A F_{S}^{'} (x))$
103		0cnd	$⊢ (φ \land x \in X) \to 0 \in ℂ$
104		ovexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) A \in V$
105	72	oveq1d	$⊢ φ \to {(X \times \{A\})}_{S}^{'} \times_{f} F = (X \times \{0\}) \times_{f} F$
106		0cnd	$⊢ φ \to 0 \in ℂ$
107		mul02	$⊢ x \in ℂ \to 0 \cdot x = 0$
108	107	adantl	$⊢ (φ \land x \in ℂ) \to 0 \cdot x = 0$
109	82 2 106 106 108	caofid2	$⊢ φ \to (X \times \{0\}) \times_{f} F = X \times \{0\}$
110	105 109	eqtrd	$⊢ φ \to {(X \times \{A\})}_{S}^{'} \times_{f} F = X \times \{0\}$
111	110 69	eqtrdi	$⊢ φ \to {(X \times \{A\})}_{S}^{'} \times_{f} F = (x \in X ⟼ 0)$
112		fvexd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) \in V$
113	3	adantr	$⊢ (φ \land x \in X) \to A \in ℂ$
114	99	feqmptd	$⊢ φ \to S D F = (x \in X ⟼ F_{S}^{'} (x))$
115	27	a1i	$⊢ φ \to X \times \{A\} = (x \in X ⟼ A)$
116	82 112 113 114 115	offval2	$⊢ φ \to F_{S}^{'} \times_{f} (X \times \{A\}) = (x \in X ⟼ F_{S}^{'} (x) A)$
117	82 103 104 111 116	offval2	$⊢ φ \to ({(X \times \{A\})}_{S}^{'} \times_{f} F) +_{f} (F_{S}^{'} \times_{f} (X \times \{A\})) = (x \in X ⟼ 0 + F_{S}^{'} (x) A)$
118	99	ffvelcdmda	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) \in ℂ$
119	118 113	mulcld	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) A \in ℂ$
120	119	addlidd	$⊢ (φ \land x \in X) \to 0 + F_{S}^{'} (x) A = F_{S}^{'} (x) A$
121	118 113	mulcomd	$⊢ (φ \land x \in X) \to F_{S}^{'} (x) A = A F_{S}^{'} (x)$
122	120 121	eqtrd	$⊢ (φ \land x \in X) \to 0 + F_{S}^{'} (x) A = A F_{S}^{'} (x)$
123	122	mpteq2dva	$⊢ φ \to (x \in X ⟼ 0 + F_{S}^{'} (x) A) = (x \in X ⟼ A F_{S}^{'} (x))$
124	117 123	eqtrd	$⊢ φ \to ({(X \times \{A\})}_{S}^{'} \times_{f} F) +_{f} (F_{S}^{'} \times_{f} (X \times \{A\})) = (x \in X ⟼ A F_{S}^{'} (x))$
125	95 102 124	3eqtr4d	$⊢ φ \to (S \times \{A\}) \times_{f} F_{S}^{'} = ({(X \times \{A\})}_{S}^{'} \times_{f} F) +_{f} (F_{S}^{'} \times_{f} (X \times \{A\}))$
126	76 94 125	3eqtr4d	$⊢ φ \to S D ((S \times \{A\}) \times_{f} F) = (S \times \{A\}) \times_{f} F_{S}^{'}$

Metamath Proof Explorer

Theorem dvcmulf

Proof