Metamath Proof Explorer

Theorem mulc1cncfg

Description: A version of mulc1cncf using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses mulc1cncfg.1 
|- F/_ x F
mulc1cncfg.2 
|- F/ x ph
mulc1cncfg.3 
|- ( ph -> F e. ( A -cn-> CC ) )
mulc1cncfg.4 
|- ( ph -> B e. CC )
Assertion mulc1cncfg 
|- ( ph -> ( x e. A |-> ( B x. ( F ` x ) ) ) e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 mulc1cncfg.1 
 |-  F/_ x F
2 mulc1cncfg.2 
 |-  F/ x ph
3 mulc1cncfg.3 
 |-  ( ph -> F e. ( A -cn-> CC ) )
4 mulc1cncfg.4 
 |-  ( ph -> B e. CC )
5 eqid 
 |-  ( x e. CC |-> ( B x. x ) ) = ( x e. CC |-> ( B x. x ) )
6 5 mulc1cncf 
 |-  ( B e. CC -> ( x e. CC |-> ( B x. x ) ) e. ( CC -cn-> CC ) )
7 4 6 syl 
 |-  ( ph -> ( x e. CC |-> ( B x. x ) ) e. ( CC -cn-> CC ) )
8 cncff 
 |-  ( ( x e. CC |-> ( B x. x ) ) e. ( CC -cn-> CC ) -> ( x e. CC |-> ( B x. x ) ) : CC --> CC )
9 7 8 syl 
 |-  ( ph -> ( x e. CC |-> ( B x. x ) ) : CC --> CC )
10 cncff 
 |-  ( F e. ( A -cn-> CC ) -> F : A --> CC )
11 3 10 syl 
 |-  ( ph -> F : A --> CC )
12 fcompt 
 |-  ( ( ( x e. CC |-> ( B x. x ) ) : CC --> CC /\ F : A --> CC ) -> ( ( x e. CC |-> ( B x. x ) ) o. F ) = ( t e. A |-> ( ( x e. CC |-> ( B x. x ) ) ` ( F ` t ) ) ) )
13 9 11 12 syl2anc 
 |-  ( ph -> ( ( x e. CC |-> ( B x. x ) ) o. F ) = ( t e. A |-> ( ( x e. CC |-> ( B x. x ) ) ` ( F ` t ) ) ) )
14 11 ffvelrnda 
 |-  ( ( ph /\ t e. A ) -> ( F ` t ) e. CC )
15 4 adantr 
 |-  ( ( ph /\ t e. A ) -> B e. CC )
16 15 14 mulcld 
 |-  ( ( ph /\ t e. A ) -> ( B x. ( F ` t ) ) e. CC )
17 nfcv 
 |-  F/_ x t
18 1 17 nffv 
 |-  F/_ x ( F ` t )
19 nfcv 
 |-  F/_ x B
20 nfcv 
 |-  F/_ x x.
21 19 20 18 nfov 
 |-  F/_ x ( B x. ( F ` t ) )
22 oveq2 
 |-  ( x = ( F ` t ) -> ( B x. x ) = ( B x. ( F ` t ) ) )
23 18 21 22 5 fvmptf 
 |-  ( ( ( F ` t ) e. CC /\ ( B x. ( F ` t ) ) e. CC ) -> ( ( x e. CC |-> ( B x. x ) ) ` ( F ` t ) ) = ( B x. ( F ` t ) ) )
24 14 16 23 syl2anc 
 |-  ( ( ph /\ t e. A ) -> ( ( x e. CC |-> ( B x. x ) ) ` ( F ` t ) ) = ( B x. ( F ` t ) ) )
25 24 mpteq2dva 
 |-  ( ph -> ( t e. A |-> ( ( x e. CC |-> ( B x. x ) ) ` ( F ` t ) ) ) = ( t e. A |-> ( B x. ( F ` t ) ) ) )
26 nfcv 
 |-  F/_ t B
27 nfcv 
 |-  F/_ t x.
28 nfcv 
 |-  F/_ t ( F ` x )
29 26 27 28 nfov 
 |-  F/_ t ( B x. ( F ` x ) )
30 fveq2 
 |-  ( t = x -> ( F ` t ) = ( F ` x ) )
31 30 oveq2d 
 |-  ( t = x -> ( B x. ( F ` t ) ) = ( B x. ( F ` x ) ) )
32 21 29 31 cbvmpt 
 |-  ( t e. A |-> ( B x. ( F ` t ) ) ) = ( x e. A |-> ( B x. ( F ` x ) ) )
33 25 32 eqtrdi 
 |-  ( ph -> ( t e. A |-> ( ( x e. CC |-> ( B x. x ) ) ` ( F ` t ) ) ) = ( x e. A |-> ( B x. ( F ` x ) ) ) )
34 13 33 eqtrd 
 |-  ( ph -> ( ( x e. CC |-> ( B x. x ) ) o. F ) = ( x e. A |-> ( B x. ( F ` x ) ) ) )
35 3 7 cncfco 
 |-  ( ph -> ( ( x e. CC |-> ( B x. x ) ) o. F ) e. ( A -cn-> CC ) )
36 34 35 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( B x. ( F ` x ) ) ) e. ( A -cn-> CC ) )