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	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 · 𝐵 ) )