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	$$⊢Ⅎk\phi$$
	climmulf.2	$$⊢\underset{\_}{Ⅎ}kF$$
	climmulf.3	$$⊢\underset{\_}{Ⅎ}kG$$
	climmulf.4	$$⊢\underset{\_}{Ⅎ}kH$$
	climmulf.5	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climmulf.6	$$⊢\phi \to M\in \mathbb{Z}$$
	climmulf.7	$$⊢\phi \to F⇝A$$
	climmulf.8	$$⊢\phi \to H\in X$$
	climmulf.9	$$⊢\phi \to G⇝B$$
	climmulf.10	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	climmulf.11	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
	climmulf.12	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(k\right)G\left(k\right)$$
Assertion	climmulf	$$⊢\phi \to H⇝AB$$

Proof

Step	Hyp	Ref	Expression
1		climmulf.1	$$⊢Ⅎk\phi$$
2		climmulf.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		climmulf.3	$$⊢\underset{\_}{Ⅎ}kG$$
4		climmulf.4	$$⊢\underset{\_}{Ⅎ}kH$$
5		climmulf.5	$$⊢Z={\mathbb{Z}}_{\ge M}$$
6		climmulf.6	$$⊢\phi \to M\in \mathbb{Z}$$
7		climmulf.7	$$⊢\phi \to F⇝A$$
8		climmulf.8	$$⊢\phi \to H\in X$$
9		climmulf.9	$$⊢\phi \to G⇝B$$
10		climmulf.10	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
11		climmulf.11	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
12		climmulf.12	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(k\right)G\left(k\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
14	13	nfel1	$$⊢Ⅎkj\in Z$$
15	1 14	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
16	2 13	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
17	16	nfel1	$$⊢ℲkF\left(j\right)\in ℂ$$
18	15 17	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℂ\right)$$
19		eleq1w	$$⊢k=j\to \left(k\in Z\leftrightarrow j\in Z\right)$$
20	19	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in Z\right)\leftrightarrow \left(\phi \wedge j\in Z\right)\right)$$
21		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
22	21	eleq1d	$$⊢k=j\to \left(F\left(k\right)\in ℂ\leftrightarrow F\left(j\right)\in ℂ\right)$$
23	20 22	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℂ\right)\right)$$
24	18 23 10	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℂ$$
25	3 13	nffv	$$⊢\underset{\_}{Ⅎ}kG\left(j\right)$$
26	25	nfel1	$$⊢ℲkG\left(j\right)\in ℂ$$
27	15 26	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to G\left(j\right)\in ℂ\right)$$
28		fveq2	$$⊢k=j\to G\left(k\right)=G\left(j\right)$$
29	28	eleq1d	$$⊢k=j\to \left(G\left(k\right)\in ℂ\leftrightarrow G\left(j\right)\in ℂ\right)$$
30	20 29	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to G\left(j\right)\in ℂ\right)\right)$$
31	27 30 11	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to G\left(j\right)\in ℂ$$
32	4 13	nffv	$$⊢\underset{\_}{Ⅎ}kH\left(j\right)$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}k\times$$
34	16 33 25	nfov	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)G\left(j\right)$$
35	32 34	nfeq	$$⊢ℲkH\left(j\right)=F\left(j\right)G\left(j\right)$$
36	15 35	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to H\left(j\right)=F\left(j\right)G\left(j\right)\right)$$
37		fveq2	$$⊢k=j\to H\left(k\right)=H\left(j\right)$$
38	21 28	oveq12d	$$⊢k=j\to F\left(k\right)G\left(k\right)=F\left(j\right)G\left(j\right)$$
39	37 38	eqeq12d	$$⊢k=j\to \left(H\left(k\right)=F\left(k\right)G\left(k\right)\leftrightarrow H\left(j\right)=F\left(j\right)G\left(j\right)\right)$$
40	20 39	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(k\right)G\left(k\right)\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to H\left(j\right)=F\left(j\right)G\left(j\right)\right)\right)$$
41	36 40 12	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to H\left(j\right)=F\left(j\right)G\left(j\right)$$
42	5 6 7 8 9 24 31 41	climmul	$$⊢\phi \to H⇝AB$$