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