This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem negcncf

Description: The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypothesis negcncf.1 
|- F = ( x e. A |-> -u x )
Assertion negcncf 
|- ( A C_ CC -> F e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 negcncf.1 
 |-  F = ( x e. A |-> -u x )
2 neg1cn 
 |-  -u 1 e. CC
3 ssel2 
 |-  ( ( A C_ CC /\ x e. A ) -> x e. CC )
4 ovmpot 
 |-  ( ( -u 1 e. CC /\ x e. CC ) -> ( -u 1 ( a e. CC , b e. CC |-> ( a x. b ) ) x ) = ( -u 1 x. x ) )
5 4 eqcomd 
 |-  ( ( -u 1 e. CC /\ x e. CC ) -> ( -u 1 x. x ) = ( -u 1 ( a e. CC , b e. CC |-> ( a x. b ) ) x ) )
6 2 3 5 sylancr 
 |-  ( ( A C_ CC /\ x e. A ) -> ( -u 1 x. x ) = ( -u 1 ( a e. CC , b e. CC |-> ( a x. b ) ) x ) )
7 3 mulm1d 
 |-  ( ( A C_ CC /\ x e. A ) -> ( -u 1 x. x ) = -u x )
8 6 7 eqtr3d 
 |-  ( ( A C_ CC /\ x e. A ) -> ( -u 1 ( a e. CC , b e. CC |-> ( a x. b ) ) x ) = -u x )
9 8 mpteq2dva 
 |-  ( A C_ CC -> ( x e. A |-> ( -u 1 ( a e. CC , b e. CC |-> ( a x. b ) ) x ) ) = ( x e. A |-> -u x ) )
10 9 1 eqtr4di 
 |-  ( A C_ CC -> ( x e. A |-> ( -u 1 ( a e. CC , b e. CC |-> ( a x. b ) ) x ) ) = F )
11 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
12 11 mpomulcn 
 |-  ( a e. CC , b e. CC |-> ( a x. b ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
13 12 a1i 
 |-  ( A C_ CC -> ( a e. CC , b e. CC |-> ( a x. b ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
14 ssid 
 |-  CC C_ CC
15 cncfmptc 
 |-  ( ( -u 1 e. CC /\ A C_ CC /\ CC C_ CC ) -> ( x e. A |-> -u 1 ) e. ( A -cn-> CC ) )
16 2 14 15 mp3an13 
 |-  ( A C_ CC -> ( x e. A |-> -u 1 ) e. ( A -cn-> CC ) )
17 cncfmptid 
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( x e. A |-> x ) e. ( A -cn-> CC ) )
18 14 17 mpan2 
 |-  ( A C_ CC -> ( x e. A |-> x ) e. ( A -cn-> CC ) )
19 11 13 16 18 cncfmpt2f 
 |-  ( A C_ CC -> ( x e. A |-> ( -u 1 ( a e. CC , b e. CC |-> ( a x. b ) ) x ) ) e. ( A -cn-> CC ) )
20 10 19 eqeltrrd 
 |-  ( A C_ CC -> F e. ( A -cn-> CC ) )