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		ovmul	|- ( ( -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 ) )