MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsum2d2lem Structured version   Visualization version   GIF version

Theorem gsum2d2lem 19833
Description: Lemma for gsum2d2 19834: show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.)
Hypotheses
Ref Expression
gsum2d2.b 𝐵 = (Base‘𝐺)
gsum2d2.z 0 = (0g𝐺)
gsum2d2.g (𝜑𝐺 ∈ CMnd)
gsum2d2.a (𝜑𝐴𝑉)
gsum2d2.r ((𝜑𝑗𝐴) → 𝐶𝑊)
gsum2d2.f ((𝜑 ∧ (𝑗𝐴𝑘𝐶)) → 𝑋𝐵)
gsum2d2.u (𝜑𝑈 ∈ Fin)
gsum2d2.n ((𝜑 ∧ ((𝑗𝐴𝑘𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )
Assertion
Ref Expression
gsum2d2lem (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 )
Distinct variable groups:   𝑗,𝑘,𝐵   𝜑,𝑗,𝑘   𝐴,𝑗,𝑘   𝑗,𝐺,𝑘   𝑈,𝑗,𝑘   𝐶,𝑘   𝑗,𝑉   0 ,𝑗,𝑘
Allowed substitution hints:   𝐶(𝑗)   𝑉(𝑘)   𝑊(𝑗,𝑘)   𝑋(𝑗,𝑘)

Proof of Theorem gsum2d2lem
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eqid 2733 . . . 4 (𝑗𝐴, 𝑘𝐶𝑋) = (𝑗𝐴, 𝑘𝐶𝑋)
21mpofun 7527 . . 3 Fun (𝑗𝐴, 𝑘𝐶𝑋)
32a1i 11 . 2 (𝜑 → Fun (𝑗𝐴, 𝑘𝐶𝑋))
4 gsum2d2.u . . 3 (𝜑𝑈 ∈ Fin)
5 gsum2d2.f . . . . . 6 ((𝜑 ∧ (𝑗𝐴𝑘𝐶)) → 𝑋𝐵)
65ralrimivva 3201 . . . . 5 (𝜑 → ∀𝑗𝐴𝑘𝐶 𝑋𝐵)
71fmpox 8048 . . . . 5 (∀𝑗𝐴𝑘𝐶 𝑋𝐵 ↔ (𝑗𝐴, 𝑘𝐶𝑋): 𝑗𝐴 ({𝑗} × 𝐶)⟶𝐵)
86, 7sylib 217 . . . 4 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋): 𝑗𝐴 ({𝑗} × 𝐶)⟶𝐵)
9 nfv 1918 . . . . . 6 𝑗𝜑
10 nfiu1 5030 . . . . . . . 8 𝑗 𝑗𝐴 ({𝑗} × 𝐶)
11 nfcv 2904 . . . . . . . 8 𝑗𝑈
1210, 11nfdif 4124 . . . . . . 7 𝑗( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
1312nfcri 2891 . . . . . 6 𝑗 𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
149, 13nfan 1903 . . . . 5 𝑗(𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
15 nfmpo1 7484 . . . . . . 7 𝑗(𝑗𝐴, 𝑘𝐶𝑋)
16 nfcv 2904 . . . . . . 7 𝑗𝑧
1715, 16nffv 6898 . . . . . 6 𝑗((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧)
1817nfeq1 2919 . . . . 5 𝑗((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0
19 relxp 5693 . . . . . . . 8 Rel ({𝑗} × 𝐶)
2019rgenw 3066 . . . . . . 7 𝑗𝐴 Rel ({𝑗} × 𝐶)
21 reliun 5814 . . . . . . 7 (Rel 𝑗𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐶))
2220, 21mpbir 230 . . . . . 6 Rel 𝑗𝐴 ({𝑗} × 𝐶)
23 eldifi 4125 . . . . . . 7 (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → 𝑧 𝑗𝐴 ({𝑗} × 𝐶))
2423adantl 483 . . . . . 6 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐶))
25 elrel 5796 . . . . . 6 ((Rel 𝑗𝐴 ({𝑗} × 𝐶) ∧ 𝑧 𝑗𝐴 ({𝑗} × 𝐶)) → ∃𝑗𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
2622, 24, 25sylancr 588 . . . . 5 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ∃𝑗𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
27 nfv 1918 . . . . . 6 𝑘(𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
28 nfmpo2 7485 . . . . . . . 8 𝑘(𝑗𝐴, 𝑘𝐶𝑋)
29 nfcv 2904 . . . . . . . 8 𝑘𝑧
3028, 29nffv 6898 . . . . . . 7 𝑘((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧)
3130nfeq1 2919 . . . . . 6 𝑘((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0
32 simprr 772 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 = ⟨𝑗, 𝑘⟩)
3332fveq2d 6892 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩))
34 df-ov 7407 . . . . . . . . 9 (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩)
35 simprl 770 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
3632, 35eqeltrrd 2835 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
3736eldifad 3959 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐶))
38 opeliunxp 5741 . . . . . . . . . . . 12 (⟨𝑗, 𝑘⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐶) ↔ (𝑗𝐴𝑘𝐶))
3937, 38sylib 217 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗𝐴𝑘𝐶))
4039simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑗𝐴)
4139simprd 497 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑘𝐶)
4239, 5syldan 592 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋𝐵)
431ovmpt4g 7550 . . . . . . . . . 10 ((𝑗𝐴𝑘𝐶𝑋𝐵) → (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = 𝑋)
4440, 41, 42, 43syl3anc 1372 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = 𝑋)
4534, 44eqtr3id 2787 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩) = 𝑋)
46 eldifn 4126 . . . . . . . . . . . 12 (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → ¬ 𝑧𝑈)
4746ad2antrl 727 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑧𝑈)
4832eleq1d 2819 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧𝑈 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈))
49 df-br 5148 . . . . . . . . . . . 12 (𝑗𝑈𝑘 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈)
5048, 49bitr4di 289 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧𝑈𝑗𝑈𝑘))
5147, 50mtbid 324 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑗𝑈𝑘)
5239, 51jca 513 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴𝑘𝐶) ∧ ¬ 𝑗𝑈𝑘))
53 gsum2d2.n . . . . . . . . 9 ((𝜑 ∧ ((𝑗𝐴𝑘𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )
5452, 53syldan 592 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋 = 0 )
5533, 45, 543eqtrd 2777 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 )
5655expr 458 . . . . . 6 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 ))
5727, 31, 56exlimd 2212 . . . . 5 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (∃𝑘 𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 ))
5814, 18, 26, 57exlimimdd 2213 . . . 4 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 )
598, 58suppss 8174 . . 3 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ⊆ 𝑈)
604, 59ssfid 9263 . 2 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)
61 gsum2d2.a . . . 4 (𝜑𝐴𝑉)
62 gsum2d2.r . . . . 5 ((𝜑𝑗𝐴) → 𝐶𝑊)
6362ralrimiva 3147 . . . 4 (𝜑 → ∀𝑗𝐴 𝐶𝑊)
641mpoexxg 8057 . . . 4 ((𝐴𝑉 ∧ ∀𝑗𝐴 𝐶𝑊) → (𝑗𝐴, 𝑘𝐶𝑋) ∈ V)
6561, 63, 64syl2anc 585 . . 3 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋) ∈ V)
66 gsum2d2.z . . . . 5 0 = (0g𝐺)
6766fvexi 6902 . . . 4 0 ∈ V
6867a1i 11 . . 3 (𝜑0 ∈ V)
69 isfsupp 9361 . . 3 (((𝑗𝐴, 𝑘𝐶𝑋) ∈ V ∧ 0 ∈ V) → ((𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 ↔ (Fun (𝑗𝐴, 𝑘𝐶𝑋) ∧ ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)))
7065, 68, 69syl2anc 585 . 2 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 ↔ (Fun (𝑗𝐴, 𝑘𝐶𝑋) ∧ ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)))
713, 60, 70mpbir2and 712 1 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  wral 3062  Vcvv 3475  cdif 3944  {csn 4627  cop 4633   ciun 4996   class class class wbr 5147   × cxp 5673  Rel wrel 5680  Fun wfun 6534  wf 6536  cfv 6540  (class class class)co 7404  cmpo 7406   supp csupp 8141  Fincfn 8935   finSupp cfsupp 9357  Basecbs 17140  0gc0g 17381  CMndccmn 19641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  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-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 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-1o 8461  df-en 8936  df-fin 8939  df-fsupp 9358
This theorem is referenced by:  gsum2d2  19834  gsumcom2  19835
  Copyright terms: Public domain W3C validator