This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑘 𝜑
climmulf.2 ⊢ Ⅎ 𝑘 𝐹
climmulf.3 ⊢ Ⅎ 𝑘 𝐺
climmulf.4 ⊢ Ⅎ 𝑘 𝐻
climmulf.5 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climmulf.6 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climmulf.7 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climmulf.8 ⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
climmulf.9 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
climmulf.10 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
climmulf.11 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
climmulf.12 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
Assertion climmulf ( 𝜑 → 𝐻 ⇝ ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 climmulf.1 ⊢ Ⅎ 𝑘 𝜑
2 climmulf.2 ⊢ Ⅎ 𝑘 𝐹
3 climmulf.3 ⊢ Ⅎ 𝑘 𝐺
4 climmulf.4 ⊢ Ⅎ 𝑘 𝐻
5 climmulf.5 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 climmulf.6 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7 climmulf.7 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
8 climmulf.8 ⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
9 climmulf.9 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
10 climmulf.10 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
11 climmulf.11 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
12 climmulf.12 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
13 nfcv ⊢ Ⅎ 𝑘 𝑗
14 13 nfel1 ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
15 1 14 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
16 2 13 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
17 16 nfel1 ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) ∈ ℂ
18 15 17 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
19 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
20 19 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
21 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
22 21 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) )
23 20 22 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ) )
24 18 23 10 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
25 3 13 nffv ⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
26 25 nfel1 ⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 ) ∈ ℂ
27 15 26 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ )
28 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
29 28 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐺 ‘ 𝑗 ) ∈ ℂ ) )
30 20 29 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ ) ) )
31 27 30 11 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ )
32 4 13 nffv ⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 )
33 nfcv ⊢ Ⅎ 𝑘 ·
34 16 33 25 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑗 ) · ( 𝐺 ‘ 𝑗 ) )
35 32 34 nfeq ⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) · ( 𝐺 ‘ 𝑗 ) )
36 15 35 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) · ( 𝐺 ‘ 𝑗 ) ) )
37 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑗 ) )
38 21 28 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑗 ) · ( 𝐺 ‘ 𝑗 ) ) )
39 37 38 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) · ( 𝐺 ‘ 𝑗 ) ) ) )
40 20 39 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) · ( 𝐺 ‘ 𝑗 ) ) ) ) )
41 36 40 12 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) · ( 𝐺 ‘ 𝑗 ) ) )
42 5 6 7 8 9 24 31 41 climmul ⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 · 𝐵 ) )