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