Metamath Proof Explorer


Theorem climmulf

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

Ref Expression
Hypotheses climmulf.1
|- F/ k ph
climmulf.2
|- F/_ k F
climmulf.3
|- F/_ k G
climmulf.4
|- F/_ k H
climmulf.5
|- Z = ( ZZ>= ` M )
climmulf.6
|- ( ph -> M e. ZZ )
climmulf.7
|- ( ph -> F ~~> A )
climmulf.8
|- ( ph -> H e. X )
climmulf.9
|- ( ph -> G ~~> B )
climmulf.10
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climmulf.11
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
climmulf.12
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
Assertion climmulf
|- ( ph -> H ~~> ( A x. B ) )

Proof

Step Hyp Ref Expression
1 climmulf.1
 |-  F/ k ph
2 climmulf.2
 |-  F/_ k F
3 climmulf.3
 |-  F/_ k G
4 climmulf.4
 |-  F/_ k H
5 climmulf.5
 |-  Z = ( ZZ>= ` M )
6 climmulf.6
 |-  ( ph -> M e. ZZ )
7 climmulf.7
 |-  ( ph -> F ~~> A )
8 climmulf.8
 |-  ( ph -> H e. X )
9 climmulf.9
 |-  ( ph -> G ~~> B )
10 climmulf.10
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
11 climmulf.11
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
12 climmulf.12
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
13 nfcv
 |-  F/_ k j
14 13 nfel1
 |-  F/ k j e. Z
15 1 14 nfan
 |-  F/ k ( ph /\ j e. Z )
16 2 13 nffv
 |-  F/_ k ( F ` j )
17 16 nfel1
 |-  F/ k ( F ` j ) e. CC
18 15 17 nfim
 |-  F/ k ( ( ph /\ j e. Z ) -> ( F ` j ) e. CC )
19 eleq1w
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
20 19 anbi2d
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
21 fveq2
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
22 21 eleq1d
 |-  ( k = j -> ( ( F ` k ) e. CC <-> ( F ` j ) e. CC ) )
23 20 22 imbi12d
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) <-> ( ( ph /\ j e. Z ) -> ( F ` j ) e. CC ) ) )
24 18 23 10 chvarfv
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. CC )
25 3 13 nffv
 |-  F/_ k ( G ` j )
26 25 nfel1
 |-  F/ k ( G ` j ) e. CC
27 15 26 nfim
 |-  F/ k ( ( ph /\ j e. Z ) -> ( G ` j ) e. CC )
28 fveq2
 |-  ( k = j -> ( G ` k ) = ( G ` j ) )
29 28 eleq1d
 |-  ( k = j -> ( ( G ` k ) e. CC <-> ( G ` j ) e. CC ) )
30 20 29 imbi12d
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC ) <-> ( ( ph /\ j e. Z ) -> ( G ` j ) e. CC ) ) )
31 27 30 11 chvarfv
 |-  ( ( ph /\ j e. Z ) -> ( G ` j ) e. CC )
32 4 13 nffv
 |-  F/_ k ( H ` j )
33 nfcv
 |-  F/_ k x.
34 16 33 25 nfov
 |-  F/_ k ( ( F ` j ) x. ( G ` j ) )
35 32 34 nfeq
 |-  F/ k ( H ` j ) = ( ( F ` j ) x. ( G ` j ) )
36 15 35 nfim
 |-  F/ k ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) x. ( G ` j ) ) )
37 fveq2
 |-  ( k = j -> ( H ` k ) = ( H ` j ) )
38 21 28 oveq12d
 |-  ( k = j -> ( ( F ` k ) x. ( G ` k ) ) = ( ( F ` j ) x. ( G ` j ) ) )
39 37 38 eqeq12d
 |-  ( k = j -> ( ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) <-> ( H ` j ) = ( ( F ` j ) x. ( G ` j ) ) ) )
40 20 39 imbi12d
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) ) <-> ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) x. ( G ` j ) ) ) ) )
41 36 40 12 chvarfv
 |-  ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) x. ( G ` j ) ) )
42 5 6 7 8 9 24 31 41 climmul
 |-  ( ph -> H ~~> ( A x. B ) )