Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  reprval Structured version   Visualization version   GIF version

Theorem reprval 33610
Description: Value of the representations of 𝑀 as the sum of 𝑆 nonnegative integers in a given set 𝐴. (Contributed by Thierry Arnoux, 1-Dec-2021.)
Hypotheses
Ref Expression
reprval.a (πœ‘ β†’ 𝐴 βŠ† β„•)
reprval.m (πœ‘ β†’ 𝑀 ∈ β„€)
reprval.s (πœ‘ β†’ 𝑆 ∈ β„•0)
Assertion
Ref Expression
reprval (πœ‘ β†’ (𝐴(reprβ€˜π‘†)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
Distinct variable groups:   𝐴,𝑐   𝑀,𝑐   𝑆,π‘Ž,𝑐   πœ‘,𝑐
Allowed substitution hints:   πœ‘(π‘Ž)   𝐴(π‘Ž)   𝑀(π‘Ž)

Proof of Theorem reprval
Dummy variables 𝑏 π‘š 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-repr 33609 . . 3 repr = (𝑠 ∈ β„•0 ↦ (𝑏 ∈ 𝒫 β„•, π‘š ∈ β„€ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Ξ£π‘Ž ∈ (0..^𝑠)(π‘β€˜π‘Ž) = π‘š}))
2 oveq2 7413 . . . . . 6 (𝑠 = 𝑆 β†’ (0..^𝑠) = (0..^𝑆))
32oveq2d 7421 . . . . 5 (𝑠 = 𝑆 β†’ (𝑏 ↑m (0..^𝑠)) = (𝑏 ↑m (0..^𝑆)))
42sumeq1d 15643 . . . . . 6 (𝑠 = 𝑆 β†’ Ξ£π‘Ž ∈ (0..^𝑠)(π‘β€˜π‘Ž) = Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž))
54eqeq1d 2734 . . . . 5 (𝑠 = 𝑆 β†’ (Ξ£π‘Ž ∈ (0..^𝑠)(π‘β€˜π‘Ž) = π‘š ↔ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š))
63, 5rabeqbidv 3449 . . . 4 (𝑠 = 𝑆 β†’ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Ξ£π‘Ž ∈ (0..^𝑠)(π‘β€˜π‘Ž) = π‘š} = {𝑐 ∈ (𝑏 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š})
76mpoeq3dv 7484 . . 3 (𝑠 = 𝑆 β†’ (𝑏 ∈ 𝒫 β„•, π‘š ∈ β„€ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑠)) ∣ Ξ£π‘Ž ∈ (0..^𝑠)(π‘β€˜π‘Ž) = π‘š}) = (𝑏 ∈ 𝒫 β„•, π‘š ∈ β„€ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š}))
8 reprval.s . . 3 (πœ‘ β†’ 𝑆 ∈ β„•0)
9 nnex 12214 . . . . . 6 β„• ∈ V
109pwex 5377 . . . . 5 𝒫 β„• ∈ V
11 zex 12563 . . . . 5 β„€ ∈ V
1210, 11mpoex 8062 . . . 4 (𝑏 ∈ 𝒫 β„•, π‘š ∈ β„€ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š}) ∈ V
1312a1i 11 . . 3 (πœ‘ β†’ (𝑏 ∈ 𝒫 β„•, π‘š ∈ β„€ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š}) ∈ V)
141, 7, 8, 13fvmptd3 7018 . 2 (πœ‘ β†’ (reprβ€˜π‘†) = (𝑏 ∈ 𝒫 β„•, π‘š ∈ β„€ ↦ {𝑐 ∈ (𝑏 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š}))
15 simprl 769 . . . 4 ((πœ‘ ∧ (𝑏 = 𝐴 ∧ π‘š = 𝑀)) β†’ 𝑏 = 𝐴)
1615oveq1d 7420 . . 3 ((πœ‘ ∧ (𝑏 = 𝐴 ∧ π‘š = 𝑀)) β†’ (𝑏 ↑m (0..^𝑆)) = (𝐴 ↑m (0..^𝑆)))
17 simprr 771 . . . 4 ((πœ‘ ∧ (𝑏 = 𝐴 ∧ π‘š = 𝑀)) β†’ π‘š = 𝑀)
1817eqeq2d 2743 . . 3 ((πœ‘ ∧ (𝑏 = 𝐴 ∧ π‘š = 𝑀)) β†’ (Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š ↔ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀))
1916, 18rabeqbidv 3449 . 2 ((πœ‘ ∧ (𝑏 = 𝐴 ∧ π‘š = 𝑀)) β†’ {𝑐 ∈ (𝑏 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = π‘š} = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
209a1i 11 . . . 4 (πœ‘ β†’ β„• ∈ V)
21 reprval.a . . . 4 (πœ‘ β†’ 𝐴 βŠ† β„•)
2220, 21ssexd 5323 . . 3 (πœ‘ β†’ 𝐴 ∈ V)
2322, 21elpwd 4607 . 2 (πœ‘ β†’ 𝐴 ∈ 𝒫 β„•)
24 reprval.m . 2 (πœ‘ β†’ 𝑀 ∈ β„€)
25 ovex 7438 . . . 4 (𝐴 ↑m (0..^𝑆)) ∈ V
2625rabex 5331 . . 3 {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀} ∈ V
2726a1i 11 . 2 (πœ‘ β†’ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀} ∈ V)
2814, 19, 23, 24, 27ovmpod 7556 1 (πœ‘ β†’ (𝐴(reprβ€˜π‘†)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3432  Vcvv 3474   βŠ† wss 3947  π’« cpw 4601  β€˜cfv 6540  (class class class)co 7405   ∈ cmpo 7407   ↑m cmap 8816  0cc0 11106  β„•cn 12208  β„•0cn0 12468  β„€cz 12554  ..^cfzo 13623  Ξ£csu 15628  reprcrepr 33608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-addcl 11166
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-neg 11443  df-nn 12209  df-z 12555  df-seq 13963  df-sum 15629  df-repr 33609
This theorem is referenced by:  repr0  33611  reprf  33612  reprsum  33613  reprsuc  33615  reprfi  33616  reprss  33617  reprinrn  33618  reprlt  33619  reprgt  33621  reprinfz1  33622  reprpmtf1o  33626  reprdifc  33627  breprexplema  33630
  Copyright terms: Public domain W3C validator