MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvcmulf Structured version   Unicode version

Theorem dvcmulf 22214
Description: The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
Hypotheses
Ref Expression
dvcmul.s  |-  ( ph  ->  S  e.  { RR ,  CC } )
dvcmul.f  |-  ( ph  ->  F : X --> CC )
dvcmul.a  |-  ( ph  ->  A  e.  CC )
dvcmulf.df  |-  ( ph  ->  dom  ( S  _D  F )  =  X )
Assertion
Ref Expression
dvcmulf  |-  ( ph  ->  ( S  _D  (
( S  X.  { A } )  oF  x.  F ) )  =  ( ( S  X.  { A }
)  oF  x.  ( S  _D  F
) ) )

Proof of Theorem dvcmulf
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dvcmul.s . . 3  |-  ( ph  ->  S  e.  { RR ,  CC } )
2 dvcmul.a . . . . 5  |-  ( ph  ->  A  e.  CC )
3 fconstg 5758 . . . . 5  |-  ( A  e.  CC  ->  ( X  X.  { A }
) : X --> { A } )
42, 3syl 16 . . . 4  |-  ( ph  ->  ( X  X.  { A } ) : X --> { A } )
52snssd 4156 . . . 4  |-  ( ph  ->  { A }  C_  CC )
64, 5fssd 5726 . . 3  |-  ( ph  ->  ( X  X.  { A } ) : X --> CC )
7 dvcmul.f . . 3  |-  ( ph  ->  F : X --> CC )
8 c0ex 9588 . . . . . 6  |-  0  e.  _V
98fconst 5757 . . . . 5  |-  ( X  X.  { 0 } ) : X --> { 0 }
10 recnprss 22174 . . . . . . . . 9  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
111, 10syl 16 . . . . . . . 8  |-  ( ph  ->  S  C_  CC )
12 fconstg 5758 . . . . . . . . . 10  |-  ( A  e.  CC  ->  ( S  X.  { A }
) : S --> { A } )
132, 12syl 16 . . . . . . . . 9  |-  ( ph  ->  ( S  X.  { A } ) : S --> { A } )
1413, 5fssd 5726 . . . . . . . 8  |-  ( ph  ->  ( S  X.  { A } ) : S --> CC )
15 ssid 3505 . . . . . . . . 9  |-  S  C_  S
1615a1i 11 . . . . . . . 8  |-  ( ph  ->  S  C_  S )
17 dvcmulf.df . . . . . . . . 9  |-  ( ph  ->  dom  ( S  _D  F )  =  X )
18 dvbsss 22172 . . . . . . . . . 10  |-  dom  ( S  _D  F )  C_  S
1918a1i 11 . . . . . . . . 9  |-  ( ph  ->  dom  ( S  _D  F )  C_  S
)
2017, 19eqsstr3d 3521 . . . . . . . 8  |-  ( ph  ->  X  C_  S )
21 eqid 2441 . . . . . . . . 9  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
22 eqid 2441 . . . . . . . . 9  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
2321, 22dvres 22181 . . . . . . . 8  |-  ( ( ( S  C_  CC  /\  ( S  X.  { A } ) : S --> CC )  /\  ( S  C_  S  /\  X  C_  S ) )  -> 
( S  _D  (
( S  X.  { A } )  |`  X ) )  =  ( ( S  _D  ( S  X.  { A }
) )  |`  (
( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
2411, 14, 16, 20, 23syl22anc 1228 . . . . . . 7  |-  ( ph  ->  ( S  _D  (
( S  X.  { A } )  |`  X ) )  =  ( ( S  _D  ( S  X.  { A }
) )  |`  (
( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
2520resmptd 5311 . . . . . . . . 9  |-  ( ph  ->  ( ( x  e.  S  |->  A )  |`  X )  =  ( x  e.  X  |->  A ) )
26 fconstmpt 5029 . . . . . . . . . 10  |-  ( S  X.  { A }
)  =  ( x  e.  S  |->  A )
2726reseq1i 5255 . . . . . . . . 9  |-  ( ( S  X.  { A } )  |`  X )  =  ( ( x  e.  S  |->  A )  |`  X )
28 fconstmpt 5029 . . . . . . . . 9  |-  ( X  X.  { A }
)  =  ( x  e.  X  |->  A )
2925, 27, 283eqtr4g 2507 . . . . . . . 8  |-  ( ph  ->  ( ( S  X.  { A } )  |`  X )  =  ( X  X.  { A } ) )
3029oveq2d 6293 . . . . . . 7  |-  ( ph  ->  ( S  _D  (
( S  X.  { A } )  |`  X ) )  =  ( S  _D  ( X  X.  { A } ) ) )
3120resmptd 5311 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  S  |->  0 )  |`  X )  =  ( x  e.  X  |->  0 ) )
32 fconstg 5758 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  ( CC  X.  { A }
) : CC --> { A } )
332, 32syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( CC  X.  { A } ) : CC --> { A } )
3433, 5fssd 5726 . . . . . . . . . . . 12  |-  ( ph  ->  ( CC  X.  { A } ) : CC --> CC )
35 ssid 3505 . . . . . . . . . . . . 13  |-  CC  C_  CC
3635a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  CC  C_  CC )
37 dvconst 22186 . . . . . . . . . . . . . . . 16  |-  ( A  e.  CC  ->  ( CC  _D  ( CC  X.  { A } ) )  =  ( CC  X.  { 0 } ) )
382, 37syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( CC  _D  ( CC  X.  { A }
) )  =  ( CC  X.  { 0 } ) )
3938dmeqd 5191 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( CC  _D  ( CC  X.  { A } ) )  =  dom  ( CC  X.  { 0 } ) )
408fconst 5757 . . . . . . . . . . . . . . 15  |-  ( CC 
X.  { 0 } ) : CC --> { 0 }
4140fdmi 5722 . . . . . . . . . . . . . 14  |-  dom  ( CC  X.  { 0 } )  =  CC
4239, 41syl6eq 2498 . . . . . . . . . . . . 13  |-  ( ph  ->  dom  ( CC  _D  ( CC  X.  { A } ) )  =  CC )
4311, 42sseqtr4d 3523 . . . . . . . . . . . 12  |-  ( ph  ->  S  C_  dom  ( CC 
_D  ( CC  X.  { A } ) ) )
44 dvres3 22183 . . . . . . . . . . . 12  |-  ( ( ( S  e.  { RR ,  CC }  /\  ( CC  X.  { A } ) : CC --> CC )  /\  ( CC  C_  CC  /\  S  C_ 
dom  ( CC  _D  ( CC  X.  { A } ) ) ) )  ->  ( S  _D  ( ( CC  X.  { A } )  |`  S ) )  =  ( ( CC  _D  ( CC  X.  { A } ) )  |`  S ) )
451, 34, 36, 43, 44syl22anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  ( S  _D  (
( CC  X.  { A } )  |`  S ) )  =  ( ( CC  _D  ( CC 
X.  { A }
) )  |`  S ) )
46 xpssres 5294 . . . . . . . . . . . . 13  |-  ( S 
C_  CC  ->  ( ( CC  X.  { A } )  |`  S )  =  ( S  X.  { A } ) )
4711, 46syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( CC  X.  { A } )  |`  S )  =  ( S  X.  { A } ) )
4847oveq2d 6293 . . . . . . . . . . 11  |-  ( ph  ->  ( S  _D  (
( CC  X.  { A } )  |`  S ) )  =  ( S  _D  ( S  X.  { A } ) ) )
4938reseq1d 5258 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( CC  _D  ( CC  X.  { A } ) )  |`  S )  =  ( ( CC  X.  {
0 } )  |`  S ) )
50 xpssres 5294 . . . . . . . . . . . . 13  |-  ( S 
C_  CC  ->  ( ( CC  X.  { 0 } )  |`  S )  =  ( S  X.  { 0 } ) )
5111, 50syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( CC  X.  { 0 } )  |`  S )  =  ( S  X.  { 0 } ) )
5249, 51eqtrd 2482 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  _D  ( CC  X.  { A } ) )  |`  S )  =  ( S  X.  { 0 } ) )
5345, 48, 523eqtr3d 2490 . . . . . . . . . 10  |-  ( ph  ->  ( S  _D  ( S  X.  { A }
) )  =  ( S  X.  { 0 } ) )
54 fconstmpt 5029 . . . . . . . . . 10  |-  ( S  X.  { 0 } )  =  ( x  e.  S  |->  0 )
5553, 54syl6eq 2498 . . . . . . . . 9  |-  ( ph  ->  ( S  _D  ( S  X.  { A }
) )  =  ( x  e.  S  |->  0 ) )
5621cnfldtopon 21156 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
57 resttopon 19528 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
5856, 11, 57sylancr 663 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
59 topontop 19294 . . . . . . . . . . . 12  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  (
( TopOpen ` fld )t  S )  e.  Top )
6058, 59syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  Top )
61 toponuni 19295 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
6258, 61syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  S  =  U. (
( TopOpen ` fld )t  S ) )
6320, 62sseqtrd 3522 . . . . . . . . . . 11  |-  ( ph  ->  X  C_  U. (
( TopOpen ` fld )t  S ) )
64 eqid 2441 . . . . . . . . . . . 12  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
6564ntrss2 19424 . . . . . . . . . . 11  |-  ( ( ( ( TopOpen ` fld )t  S )  e.  Top  /\  X  C_  U. (
( TopOpen ` fld )t  S ) )  -> 
( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
6660, 63, 65syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
6711, 7, 20, 22, 21dvbssntr 22170 . . . . . . . . . . 11  |-  ( ph  ->  dom  ( S  _D  F )  C_  (
( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
6817, 67eqsstr3d 3521 . . . . . . . . . 10  |-  ( ph  ->  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
6966, 68eqssd 3503 . . . . . . . . 9  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  =  X )
7055, 69reseq12d 5260 . . . . . . . 8  |-  ( ph  ->  ( ( S  _D  ( S  X.  { A } ) )  |`  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )  =  ( ( x  e.  S  |->  0 )  |`  X ) )
71 fconstmpt 5029 . . . . . . . . 9  |-  ( X  X.  { 0 } )  =  ( x  e.  X  |->  0 )
7271a1i 11 . . . . . . . 8  |-  ( ph  ->  ( X  X.  {
0 } )  =  ( x  e.  X  |->  0 ) )
7331, 70, 723eqtr4d 2492 . . . . . . 7  |-  ( ph  ->  ( ( S  _D  ( S  X.  { A } ) )  |`  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )  =  ( X  X.  {
0 } ) )
7424, 30, 733eqtr3d 2490 . . . . . 6  |-  ( ph  ->  ( S  _D  ( X  X.  { A }
) )  =  ( X  X.  { 0 } ) )
7574feq1d 5703 . . . . 5  |-  ( ph  ->  ( ( S  _D  ( X  X.  { A } ) ) : X --> { 0 }  <-> 
( X  X.  {
0 } ) : X --> { 0 } ) )
769, 75mpbiri 233 . . . 4  |-  ( ph  ->  ( S  _D  ( X  X.  { A }
) ) : X --> { 0 } )
77 fdm 5721 . . . 4  |-  ( ( S  _D  ( X  X.  { A }
) ) : X --> { 0 }  ->  dom  ( S  _D  ( X  X.  { A }
) )  =  X )
7876, 77syl 16 . . 3  |-  ( ph  ->  dom  ( S  _D  ( X  X.  { A } ) )  =  X )
791, 6, 7, 78, 17dvmulf 22212 . 2  |-  ( ph  ->  ( S  _D  (
( X  X.  { A } )  oF  x.  F ) )  =  ( ( ( S  _D  ( X  X.  { A }
) )  oF  x.  F )  oF  +  ( ( S  _D  F )  oF  x.  ( X  X.  { A }
) ) ) )
80 sseqin2 3699 . . . . . 6  |-  ( X 
C_  S  <->  ( S  i^i  X )  =  X )
8120, 80sylib 196 . . . . 5  |-  ( ph  ->  ( S  i^i  X
)  =  X )
8281mpteq1d 4514 . . . 4  |-  ( ph  ->  ( x  e.  ( S  i^i  X ) 
|->  ( A  x.  ( F `  x )
) )  =  ( x  e.  X  |->  ( A  x.  ( F `
 x ) ) ) )
83 ffn 5717 . . . . . 6  |-  ( ( S  X.  { A } ) : S --> { A }  ->  ( S  X.  { A }
)  Fn  S )
8413, 83syl 16 . . . . 5  |-  ( ph  ->  ( S  X.  { A } )  Fn  S
)
85 ffn 5717 . . . . . 6  |-  ( F : X --> CC  ->  F  Fn  X )
867, 85syl 16 . . . . 5  |-  ( ph  ->  F  Fn  X )
871, 20ssexd 4580 . . . . 5  |-  ( ph  ->  X  e.  _V )
88 eqid 2441 . . . . 5  |-  ( S  i^i  X )  =  ( S  i^i  X
)
89 fvconst2g 6105 . . . . . 6  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( S  X.  { A } ) `  x )  =  A )
902, 89sylan 471 . . . . 5  |-  ( (
ph  /\  x  e.  S )  ->  (
( S  X.  { A } ) `  x
)  =  A )
91 eqidd 2442 . . . . 5  |-  ( (
ph  /\  x  e.  X )  ->  ( F `  x )  =  ( F `  x ) )
9284, 86, 1, 87, 88, 90, 91offval 6528 . . . 4  |-  ( ph  ->  ( ( S  X.  { A } )  oF  x.  F )  =  ( x  e.  ( S  i^i  X
)  |->  ( A  x.  ( F `  x ) ) ) )
93 ffn 5717 . . . . . 6  |-  ( ( X  X.  { A } ) : X --> { A }  ->  ( X  X.  { A }
)  Fn  X )
944, 93syl 16 . . . . 5  |-  ( ph  ->  ( X  X.  { A } )  Fn  X
)
95 inidm 3689 . . . . 5  |-  ( X  i^i  X )  =  X
96 fvconst2g 6105 . . . . . 6  |-  ( ( A  e.  CC  /\  x  e.  X )  ->  ( ( X  X.  { A } ) `  x )  =  A )
972, 96sylan 471 . . . . 5  |-  ( (
ph  /\  x  e.  X )  ->  (
( X  X.  { A } ) `  x
)  =  A )
9894, 86, 87, 87, 95, 97, 91offval 6528 . . . 4  |-  ( ph  ->  ( ( X  X.  { A } )  oF  x.  F )  =  ( x  e.  X  |->  ( A  x.  ( F `  x ) ) ) )
9982, 92, 983eqtr4d 2492 . . 3  |-  ( ph  ->  ( ( S  X.  { A } )  oF  x.  F )  =  ( ( X  X.  { A }
)  oF  x.  F ) )
10099oveq2d 6293 . 2  |-  ( ph  ->  ( S  _D  (
( S  X.  { A } )  oF  x.  F ) )  =  ( S  _D  ( ( X  X.  { A } )  oF  x.  F ) ) )
10181mpteq1d 4514 . . 3  |-  ( ph  ->  ( x  e.  ( S  i^i  X ) 
|->  ( A  x.  (
( S  _D  F
) `  x )
) )  =  ( x  e.  X  |->  ( A  x.  ( ( S  _D  F ) `
 x ) ) ) )
102 dvfg 22176 . . . . . . 7  |-  ( S  e.  { RR ,  CC }  ->  ( S  _D  F ) : dom  ( S  _D  F
) --> CC )
1031, 102syl 16 . . . . . 6  |-  ( ph  ->  ( S  _D  F
) : dom  ( S  _D  F ) --> CC )
10417feq2d 5704 . . . . . 6  |-  ( ph  ->  ( ( S  _D  F ) : dom  ( S  _D  F
) --> CC  <->  ( S  _D  F ) : X --> CC ) )
105103, 104mpbid 210 . . . . 5  |-  ( ph  ->  ( S  _D  F
) : X --> CC )
106 ffn 5717 . . . . 5  |-  ( ( S  _D  F ) : X --> CC  ->  ( S  _D  F )  Fn  X )
107105, 106syl 16 . . . 4  |-  ( ph  ->  ( S  _D  F
)  Fn  X )
108 eqidd 2442 . . . 4  |-  ( (
ph  /\  x  e.  X )  ->  (
( S  _D  F
) `  x )  =  ( ( S  _D  F ) `  x ) )
10984, 107, 1, 87, 88, 90, 108offval 6528 . . 3  |-  ( ph  ->  ( ( S  X.  { A } )  oF  x.  ( S  _D  F ) )  =  ( x  e.  ( S  i^i  X
)  |->  ( A  x.  ( ( S  _D  F ) `  x
) ) ) )
110 0cnd 9587 . . . . 5  |-  ( (
ph  /\  x  e.  X )  ->  0  e.  CC )
111 ovex 6305 . . . . . 6  |-  ( ( ( S  _D  F
) `  x )  x.  A )  e.  _V
112111a1i 11 . . . . 5  |-  ( (
ph  /\  x  e.  X )  ->  (
( ( S  _D  F ) `  x
)  x.  A )  e.  _V )
11374oveq1d 6292 . . . . . . 7  |-  ( ph  ->  ( ( S  _D  ( X  X.  { A } ) )  oF  x.  F )  =  ( ( X  X.  { 0 } )  oF  x.  F ) )
114 0cnd 9587 . . . . . . . 8  |-  ( ph  ->  0  e.  CC )
115 mul02 9756 . . . . . . . . 9  |-  ( x  e.  CC  ->  (
0  x.  x )  =  0 )
116115adantl 466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  CC )  ->  ( 0  x.  x )  =  0 )
11787, 7, 114, 114, 116caofid2 6552 . . . . . . 7  |-  ( ph  ->  ( ( X  X.  { 0 } )  oF  x.  F
)  =  ( X  X.  { 0 } ) )
118113, 117eqtrd 2482 . . . . . 6  |-  ( ph  ->  ( ( S  _D  ( X  X.  { A } ) )  oF  x.  F )  =  ( X  X.  { 0 } ) )
119118, 71syl6eq 2498 . . . . 5  |-  ( ph  ->  ( ( S  _D  ( X  X.  { A } ) )  oF  x.  F )  =  ( x  e.  X  |->  0 ) )
120 fvex 5862 . . . . . . 7  |-  ( ( S  _D  F ) `
 x )  e. 
_V
121120a1i 11 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  (
( S  _D  F
) `  x )  e.  _V )
1222adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  A  e.  CC )
123105feqmptd 5907 . . . . . 6  |-  ( ph  ->  ( S  _D  F
)  =  ( x  e.  X  |->  ( ( S  _D  F ) `
 x ) ) )
12428a1i 11 . . . . . 6  |-  ( ph  ->  ( X  X.  { A } )  =  ( x  e.  X  |->  A ) )
12587, 121, 122, 123, 124offval2 6537 . . . . 5  |-  ( ph  ->  ( ( S  _D  F )  oF  x.  ( X  X.  { A } ) )  =  ( x  e.  X  |->  ( ( ( S  _D  F ) `
 x )  x.  A ) ) )
12687, 110, 112, 119, 125offval2 6537 . . . 4  |-  ( ph  ->  ( ( ( S  _D  ( X  X.  { A } ) )  oF  x.  F
)  oF  +  ( ( S  _D  F )  oF  x.  ( X  X.  { A } ) ) )  =  ( x  e.  X  |->  ( 0  +  ( ( ( S  _D  F ) `
 x )  x.  A ) ) ) )
127105ffvelrnda 6012 . . . . . . . 8  |-  ( (
ph  /\  x  e.  X )  ->  (
( S  _D  F
) `  x )  e.  CC )
128127, 122mulcld 9614 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  (
( ( S  _D  F ) `  x
)  x.  A )  e.  CC )
129128addid2d 9779 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  (
0  +  ( ( ( S  _D  F
) `  x )  x.  A ) )  =  ( ( ( S  _D  F ) `  x )  x.  A
) )
130127, 122mulcomd 9615 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  (
( ( S  _D  F ) `  x
)  x.  A )  =  ( A  x.  ( ( S  _D  F ) `  x
) ) )
131129, 130eqtrd 2482 . . . . 5  |-  ( (
ph  /\  x  e.  X )  ->  (
0  +  ( ( ( S  _D  F
) `  x )  x.  A ) )  =  ( A  x.  (
( S  _D  F
) `  x )
) )
132131mpteq2dva 4519 . . . 4  |-  ( ph  ->  ( x  e.  X  |->  ( 0  +  ( ( ( S  _D  F ) `  x
)  x.  A ) ) )  =  ( x  e.  X  |->  ( A  x.  ( ( S  _D  F ) `
 x ) ) ) )
133126, 132eqtrd 2482 . . 3  |-  ( ph  ->  ( ( ( S  _D  ( X  X.  { A } ) )  oF  x.  F
)  oF  +  ( ( S  _D  F )  oF  x.  ( X  X.  { A } ) ) )  =  ( x  e.  X  |->  ( A  x.  ( ( S  _D  F ) `  x ) ) ) )
134101, 109, 1333eqtr4d 2492 . 2  |-  ( ph  ->  ( ( S  X.  { A } )  oF  x.  ( S  _D  F ) )  =  ( ( ( S  _D  ( X  X.  { A }
) )  oF  x.  F )  oF  +  ( ( S  _D  F )  oF  x.  ( X  X.  { A }
) ) ) )
13579, 100, 1343eqtr4d 2492 1  |-  ( ph  ->  ( S  _D  (
( S  X.  { A } )  oF  x.  F ) )  =  ( ( S  X.  { A }
)  oF  x.  ( S  _D  F
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1381    e. wcel 1802   _Vcvv 3093    i^i cin 3457    C_ wss 3458   {csn 4010   {cpr 4012   U.cuni 4230    |-> cmpt 4491    X. cxp 4983   dom cdm 4985    |` cres 4987    Fn wfn 5569   -->wf 5570   ` cfv 5574  (class class class)co 6277    oFcof 6519   CCcc 9488   RRcr 9489   0cc0 9490    + caddc 9493    x. cmul 9495   ↾t crest 14690   TopOpenctopn 14691  ℂfldccnfld 18288   Topctop 19261  TopOnctopon 19262   intcnt 19384    _D cdv 22133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-inf2 8056  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568  ax-addf 9569  ax-mulf 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-iin 4314  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-se 4825  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-isom 5583  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6521  df-om 6682  df-1st 6781  df-2nd 6782  df-supp 6900  df-recs 7040  df-rdg 7074  df-1o 7128  df-2o 7129  df-oadd 7132  df-er 7309  df-map 7420  df-pm 7421  df-ixp 7468  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-fsupp 7828  df-fi 7869  df-sup 7899  df-oi 7933  df-card 8318  df-cda 8546  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-9 10602  df-10 10603  df-n0 10797  df-z 10866  df-dec 10980  df-uz 11086  df-q 11187  df-rp 11225  df-xneg 11322  df-xadd 11323  df-xmul 11324  df-icc 11540  df-fz 11677  df-fzo 11799  df-seq 12082  df-exp 12141  df-hash 12380  df-cj 12906  df-re 12907  df-im 12908  df-sqrt 13042  df-abs 13043  df-struct 14506  df-ndx 14507  df-slot 14508  df-base 14509  df-sets 14510  df-ress 14511  df-plusg 14582  df-mulr 14583  df-starv 14584  df-sca 14585  df-vsca 14586  df-ip 14587  df-tset 14588  df-ple 14589  df-ds 14591  df-unif 14592  df-hom 14593  df-cco 14594  df-rest 14692  df-topn 14693  df-0g 14711  df-gsum 14712  df-topgen 14713  df-pt 14714  df-prds 14717  df-xrs 14771  df-qtop 14776  df-imas 14777  df-xps 14779  df-mre 14855  df-mrc 14856  df-acs 14858  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-submnd 15836  df-mulg 15929  df-cntz 16224  df-cmn 16669  df-psmet 18279  df-xmet 18280  df-met 18281  df-bl 18282  df-mopn 18283  df-fbas 18284  df-fg 18285  df-cnfld 18289  df-top 19266  df-bases 19268  df-topon 19269  df-topsp 19270  df-cld 19386  df-ntr 19387  df-cls 19388  df-nei 19465  df-lp 19503  df-perf 19504  df-cn 19594  df-cnp 19595  df-haus 19682  df-tx 19929  df-hmeo 20122  df-fil 20213  df-fm 20305  df-flim 20306  df-flf 20307  df-xms 20689  df-ms 20690  df-tms 20691  df-cncf 21248  df-limc 22136  df-dv 22137
This theorem is referenced by:  dvsinax  31608
  Copyright terms: Public domain W3C validator