Theorem dffprod 15409

Description: Special case of composite over a finite index set.

Assertion

Ref	Expression
dffprod	|- (N e. (ZZ>=` M) -> prod_k e. (M...N)GA = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))

Distinct variable groups:   y,A   y,G   y,M   y,N   y,k

Proof of Theorem dffprod

Step	Hyp	Ref	Expression
1		df-prod2 15394	. 2 |- prod_k e. (M...N)GA = if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA)
2		eluzel2 7940	. . . 4 |- (N e. (ZZ>=` M) -> M e. ZZ)
3		eluzelz 7939	. . . 4 |- (N e. (ZZ>=` M) -> N e. ZZ)
4		eluzle 7941	. . . 4 |- (N e. (ZZ>=` M) -> M <_ N)
5		simp3 1122	. . . . . . 7 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> M <_ N)
6		zssre 7692	. . . . . . . . . . . 12 |- ZZ C_ RR
7		ressxr 6857	. . . . . . . . . . . 12 |- RR C_ RR*
8	6, 7	sstri 2856	. . . . . . . . . . 11 |- ZZ C_ RR*
9	8	sseli 2848	. . . . . . . . . 10 |- (M e. ZZ -> M e. RR*)
10	8	sseli 2848	. . . . . . . . . 10 |- (N e. ZZ -> N e. RR*)
11	9, 10	anim12i 536	. . . . . . . . 9 |- ((M e. ZZ /\ N e. ZZ) -> (M e. RR* /\ N e. RR*))
12	11	3adant3 1140	. . . . . . . 8 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (M e. RR* /\ N e. RR*))
13		xrlenlt 6860	. . . . . . . 8 |- ((M e. RR* /\ N e. RR*) -> (M <_ N <-> -. N < M))
14	12, 13	syl 13	. . . . . . 7 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (M <_ N <-> -. N < M))
15	5, 14	mpbid 317	. . . . . 6 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> -. N < M)
16		fzn 8024	. . . . . . . 8 |- ((M e. ZZ /\ N e. ZZ) -> (N < M <-> (M...N) = (/)))
17	16	notbid 746	. . . . . . 7 |- ((M e. ZZ /\ N e. ZZ) -> (-. N < M <-> -. (M...N) = (/)))
18	17	3adant3 1140	. . . . . 6 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (-. N < M <-> -. (M...N) = (/)))
19	15, 18	mpbid 317	. . . . 5 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> -. (M...N) = (/))
20		iffalse 3186	. . . . . 6 |- (-. (M...N) = (/) -> if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = prod3 k e. (M...N)GA)
21		df-prod 15392	. . . . . . . 8 |- prod3 k e. (M...N)GA = {x | E.mE.n e. (ZZ>=` m)((M...N) = (m...n) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))}
22		visset 2541	. . . . . . . . . . . . . . 15 |- n e. _V
23		fzopth 8037	. . . . . . . . . . . . . . 15 |- ((N e. (ZZ>=` M) /\ n e. _V) -> ((M...N) = (m...n) <-> (M = m /\ N = n)))
24	22, 23	mpan2 679	. . . . . . . . . . . . . 14 |- (N e. (ZZ>=` M) -> ((M...N) = (m...n) <-> (M = m /\ N = n)))
25		eqcom 2143	. . . . . . . . . . . . . . 15 |- (M = m <-> m = M)
26		eqcom 2143	. . . . . . . . . . . . . . 15 |- (N = n <-> n = N)
27	25, 26	anbi12i 710	. . . . . . . . . . . . . 14 |- ((M = m /\ N = n) <-> (m = M /\ n = N))
28	24, 27	syl6bb 729	. . . . . . . . . . . . 13 |- (N e. (ZZ>=` M) -> ((M...N) = (m...n) <-> (m = M /\ n = N)))
29	28	anbi1d 752	. . . . . . . . . . . 12 |- (N e. (ZZ>=` M) -> (((M...N) = (m...n) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> ((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
30	29	rexbidv 2374	. . . . . . . . . . 11 |- (N e. (ZZ>=` M) -> (E.n e. (ZZ>=` m)((M...N) = (m...n) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.n e. (ZZ>=` m)((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
31	30	exbidv 1926	. . . . . . . . . 10 |- (N e. (ZZ>=` M) -> (E.mE.n e. (ZZ>=` m)((M...N) = (m...n) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.mE.n e. (ZZ>=` m)((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
32		2rexuz 7962	. . . . . . . . . . . 12 |- (E.mE.n e. (ZZ>=` m)((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.m e. ZZ E.n e. ZZ (m <_ n /\ ((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
33		an12 844	. . . . . . . . . . . . 13 |- ((m <_ n /\ ((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
34	33	2rexbii 2380	. . . . . . . . . . . 12 |- (E.m e. ZZ E.n e. ZZ (m <_ n /\ ((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
35	32, 34	bitri 279	. . . . . . . . . . 11 |- (E.mE.n e. (ZZ>=` m)((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
36		breq1 3510	. . . . . . . . . . . . . . 15 |- (m = M -> (m <_ n <-> M <_ n))
37		opeq1 3345	. . . . . . . . . . . . . . . . . 18 |- (m = M -> <.m, G>. = <.M, G>.)
38	37	opreq1d 4993	. . . . . . . . . . . . . . . . 17 |- (m = M -> (<.m, G>. seq ({<.k, y>. | y = A} |` ZZ)) = (<.M, G>. seq ({<.k, y>. | y = A} |` ZZ)))
39	38	fveq1d 4767	. . . . . . . . . . . . . . . 16 |- (m = M -> ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))
40	39	eleq2d 2211	. . . . . . . . . . . . . . 15 |- (m = M -> (x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n) <-> x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)))
41	36, 40	anbi12d 763	. . . . . . . . . . . . . 14 |- (m = M -> ((m <_ n /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> (M <_ n /\ x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))))
42		breq2 3511	. . . . . . . . . . . . . . 15 |- (n = N -> (M <_ n <-> M <_ N))
43		fveq2 4765	. . . . . . . . . . . . . . . 16 |- (n = N -> ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` n) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))
44	43	eleq2d 2211	. . . . . . . . . . . . . . 15 |- (n = N -> (x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` n) <-> x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
45	42, 44	anbi12d 763	. . . . . . . . . . . . . 14 |- (n = N -> ((M <_ n /\ x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> (M <_ N /\ x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))))
46	41, 45	ceqsrex2v 2635	. . . . . . . . . . . . 13 |- ((M e. ZZ /\ N e. ZZ) -> (E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> (M <_ N /\ x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))))
47	2, 3, 46	syl11anc 659	. . . . . . . . . . . 12 |- (N e. (ZZ>=` M) -> (E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> (M <_ N /\ x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))))
48	4	biantrurd 956	. . . . . . . . . . . 12 |- (N e. (ZZ>=` M) -> (x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N) <-> (M <_ N /\ x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))))
49	47, 48	bitr4d 288	. . . . . . . . . . 11 |- (N e. (ZZ>=` M) -> (E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
50	35, 49	syl5bb 721	. . . . . . . . . 10 |- (N e. (ZZ>=` M) -> (E.mE.n e. (ZZ>=` m)((m = M /\ n = N) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
51	31, 50	bitrd 284	. . . . . . . . 9 |- (N e. (ZZ>=` M) -> (E.mE.n e. (ZZ>=` m)((M...N) = (m...n) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> x e. ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
52	51	abbi1dv 2259	. . . . . . . 8 |- (N e. (ZZ>=` M) -> {x | E.mE.n e. (ZZ>=` m)((M...N) = (m...n) /\ x e. ((<.m, G>. seq ({<.k, y>. | y = A} |` ZZ))` n))} = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))
53	21, 52	syl5eq 2185	. . . . . . 7 |- (N e. (ZZ>=` M) -> prod3 k e. (M...N)GA = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))
54		eqeq1 2147	. . . . . . 7 |- (if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = prod3 k e. (M...N)GA -> (if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N) <-> prod3 k e. (M...N)GA = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
55	53, 54	syl5ibr 257	. . . . . 6 |- (if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = prod3 k e. (M...N)GA -> (N e. (ZZ>=` M) -> if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
56	20, 55	syl 13	. . . . 5 |- (-. (M...N) = (/) -> (N e. (ZZ>=` M) -> if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
57	19, 56	syl 13	. . . 4 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N e. (ZZ>=` M) -> if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
58	2, 3, 4, 57	syl111anc 1349	. . 3 |- (N e. (ZZ>=` M) -> (N e. (ZZ>=` M) -> if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N)))
59	58	pm2.43i 108	. 2 |- (N e. (ZZ>=` M) -> if((M...N) = (/), (Id` G), prod3 k e. (M...N)GA) = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))
60	1, 59	syl5eq 2185	1 |- (N e. (ZZ>=` M) -> prod_k e. (M...N)GA = ((<.M, G>. seq ({<.k, y>. | y = A} |` ZZ))` N))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  E.wex 1615  {cab 2128  E.wrex 2356  _Vcvv 2538  (/)c0 3082  ifcif 3180  <.cop 3240   class class class wbr 3507  {copab 3565   |` cres 4121  ` cfv 4131  (class class class)co 4981  RRcr 6751   <_ cle 6841  RR*cxr 6844   < clt 6845  ZZcz 6994  ZZ>=cuz 7933  ...cfz 7998   seq cseqz 8149  Idcgi 10178   prod3 cprd 15391  prod_cprd2 15393

This theorem is referenced by:  fprodserz 15410  relsumprd 15423

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-ltp 6608  df-enr 6684  df-nr 6685  df-ltr 6688  df-0r 6689  df-c 6758  df-r 6762  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-neg 7011  df-z 7686  df-uz 7934  df-fz 7999  df-prod 15392  df-prod2 15394

Copyright terms: Public domain