Theorem climaddf

Description: A version of climadd using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	climaddf.1	$$⊢Ⅎk\phi$$
	climaddf.2	$$⊢\underset{\_}{Ⅎ}kF$$
	climaddf.3	$$⊢\underset{\_}{Ⅎ}kG$$
	climaddf.4	$$⊢\underset{\_}{Ⅎ}kH$$
	climaddf.5	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climaddf.6	$$⊢\phi \to M\in \mathbb{Z}$$
	climaddf.7	$$⊢\phi \to F⇝A$$
	climaddf.8	$$⊢\phi \to H\in X$$
	climaddf.9	$$⊢\phi \to G⇝B$$
	climaddf.10	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	climaddf.11	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
	climaddf.12	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(k\right)+G\left(k\right)$$
Assertion	climaddf	$$⊢\phi \to H⇝\left(A+B\right)$$

Proof

Step	Hyp	Ref	Expression
1		climaddf.1	$$⊢Ⅎk\phi$$
2		climaddf.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		climaddf.3	$$⊢\underset{\_}{Ⅎ}kG$$
4		climaddf.4	$$⊢\underset{\_}{Ⅎ}kH$$
5		climaddf.5	$$⊢Z={\mathbb{Z}}_{\ge M}$$
6		climaddf.6	$$⊢\phi \to M\in \mathbb{Z}$$
7		climaddf.7	$$⊢\phi \to F⇝A$$
8		climaddf.8	$$⊢\phi \to H\in X$$
9		climaddf.9	$$⊢\phi \to G⇝B$$
10		climaddf.10	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
11		climaddf.11	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
12		climaddf.12	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(k\right)+G\left(k\right)$$
13		nfv	$$⊢Ⅎkj\in Z$$
14	1 13	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
16	2 15	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
17	16	nfel1	$$⊢ℲkF\left(j\right)\in ℂ$$
18	14 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 15	nffv	$$⊢\underset{\_}{Ⅎ}kG\left(j\right)$$
26	25	nfel1	$$⊢ℲkG\left(j\right)\in ℂ$$
27	14 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 15	nffv	$$⊢\underset{\_}{Ⅎ}kH\left(j\right)$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}k+$$
34	16 33 25	nfov	$$⊢\underset{\_}{Ⅎ}k\left(F\left(j\right)+G\left(j\right)\right)$$
35	32 34	nfeq	$$⊢ℲkH\left(j\right)=F\left(j\right)+G\left(j\right)$$
36	14 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	climadd	$$⊢\phi \to H⇝\left(A+B\right)$$