Metamath Proof Explorer


Theorem 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 φ S
dvcmul.f φ F : X
dvcmul.a φ A
dvcmulf.df φ dom F S = X
Assertion dvcmulf φ S D S × A × f F = S × A × f F S

Proof

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