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 _ x F
mulc1cncfg.2 x φ
mulc1cncfg.3 φ F : A cn
mulc1cncfg.4 φ B
Assertion mulc1cncfg φ x A B F x : A cn

Proof

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