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

Metamath Proof Explorer

Theorem sub1cncf

Description: Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 sub1cncf.1 
 |-  F = ( x e. CC |-> ( x - A ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
4 3 a1i 
 |-  ( A e. CC -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
5 eqid 
 |-  ( x e. CC |-> x ) = ( x e. CC |-> x )
6 5 idcncf 
 |-  ( x e. CC |-> x ) e. ( CC -cn-> CC )
7 6 a1i 
 |-  ( A e. CC -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
8 ssid 
 |-  CC C_ CC
9 cncfmptc 
 |-  ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
10 8 8 9 mp3an23 
 |-  ( A e. CC -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
11 2 4 7 10 cncfmpt2f 
 |-  ( A e. CC -> ( x e. CC |-> ( x - A ) ) e. ( CC -cn-> CC ) )
12 1 11 eqeltrid 
 |-  ( A e. CC -> F e. ( CC -cn-> CC ) )