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

Theorem gsum2d2lem 19574
Description: Lemma for gsum2d2 19575: 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 2738 . . . 4 (𝑗𝐴, 𝑘𝐶𝑋) = (𝑗𝐴, 𝑘𝐶𝑋)
21mpofun 7398 . . 3 Fun (𝑗𝐴, 𝑘𝐶𝑋)
32a1i 11 . 2 (𝜑 → Fun (𝑗𝐴, 𝑘𝐶𝑋))
4 gsum2d2.u . . 3 (𝜑𝑈 ∈ Fin)
5 gsum2d2.f . . . . . 6 ((𝜑 ∧ (𝑗𝐴𝑘𝐶)) → 𝑋𝐵)
65ralrimivva 3123 . . . . 5 (𝜑 → ∀𝑗𝐴𝑘𝐶 𝑋𝐵)
71fmpox 7907 . . . . 5 (∀𝑗𝐴𝑘𝐶 𝑋𝐵 ↔ (𝑗𝐴, 𝑘𝐶𝑋): 𝑗𝐴 ({𝑗} × 𝐶)⟶𝐵)
86, 7sylib 217 . . . 4 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋): 𝑗𝐴 ({𝑗} × 𝐶)⟶𝐵)
9 nfv 1917 . . . . . 6 𝑗𝜑
10 nfiu1 4958 . . . . . . . 8 𝑗 𝑗𝐴 ({𝑗} × 𝐶)
11 nfcv 2907 . . . . . . . 8 𝑗𝑈
1210, 11nfdif 4060 . . . . . . 7 𝑗( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
1312nfcri 2894 . . . . . 6 𝑗 𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
149, 13nfan 1902 . . . . 5 𝑗(𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
15 nfmpo1 7355 . . . . . . 7 𝑗(𝑗𝐴, 𝑘𝐶𝑋)
16 nfcv 2907 . . . . . . 7 𝑗𝑧
1715, 16nffv 6784 . . . . . 6 𝑗((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧)
1817nfeq1 2922 . . . . 5 𝑗((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0
19 relxp 5607 . . . . . . . 8 Rel ({𝑗} × 𝐶)
2019rgenw 3076 . . . . . . 7 𝑗𝐴 Rel ({𝑗} × 𝐶)
21 reliun 5726 . . . . . . 7 (Rel 𝑗𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐶))
2220, 21mpbir 230 . . . . . 6 Rel 𝑗𝐴 ({𝑗} × 𝐶)
23 eldifi 4061 . . . . . . 7 (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → 𝑧 𝑗𝐴 ({𝑗} × 𝐶))
2423adantl 482 . . . . . 6 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐶))
25 elrel 5708 . . . . . 6 ((Rel 𝑗𝐴 ({𝑗} × 𝐶) ∧ 𝑧 𝑗𝐴 ({𝑗} × 𝐶)) → ∃𝑗𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
2622, 24, 25sylancr 587 . . . . 5 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ∃𝑗𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
27 nfv 1917 . . . . . 6 𝑘(𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
28 nfmpo2 7356 . . . . . . . 8 𝑘(𝑗𝐴, 𝑘𝐶𝑋)
29 nfcv 2907 . . . . . . . 8 𝑘𝑧
3028, 29nffv 6784 . . . . . . 7 𝑘((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧)
3130nfeq1 2922 . . . . . 6 𝑘((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0
32 simprr 770 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 = ⟨𝑗, 𝑘⟩)
3332fveq2d 6778 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩))
34 df-ov 7278 . . . . . . . . 9 (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩)
35 simprl 768 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
3632, 35eqeltrrd 2840 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
3736eldifad 3899 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐶))
38 opeliunxp 5654 . . . . . . . . . . . 12 (⟨𝑗, 𝑘⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐶) ↔ (𝑗𝐴𝑘𝐶))
3937, 38sylib 217 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗𝐴𝑘𝐶))
4039simpld 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑗𝐴)
4139simprd 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑘𝐶)
4239, 5syldan 591 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋𝐵)
431ovmpt4g 7420 . . . . . . . . . 10 ((𝑗𝐴𝑘𝐶𝑋𝐵) → (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = 𝑋)
4440, 41, 42, 43syl3anc 1370 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = 𝑋)
4534, 44eqtr3id 2792 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩) = 𝑋)
46 eldifn 4062 . . . . . . . . . . . 12 (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → ¬ 𝑧𝑈)
4746ad2antrl 725 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑧𝑈)
4832eleq1d 2823 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧𝑈 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈))
49 df-br 5075 . . . . . . . . . . . 12 (𝑗𝑈𝑘 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈)
5048, 49bitr4di 289 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧𝑈𝑗𝑈𝑘))
5147, 50mtbid 324 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑗𝑈𝑘)
5239, 51jca 512 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴𝑘𝐶) ∧ ¬ 𝑗𝑈𝑘))
53 gsum2d2.n . . . . . . . . 9 ((𝜑 ∧ ((𝑗𝐴𝑘𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )
5452, 53syldan 591 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋 = 0 )
5533, 45, 543eqtrd 2782 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 )
5655expr 457 . . . . . 6 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 ))
5727, 31, 56exlimd 2211 . . . . 5 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (∃𝑘 𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 ))
5814, 18, 26, 57exlimimdd 2212 . . . 4 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 )
598, 58suppss 8010 . . 3 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ⊆ 𝑈)
604, 59ssfid 9042 . 2 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)
61 gsum2d2.a . . . 4 (𝜑𝐴𝑉)
62 gsum2d2.r . . . . 5 ((𝜑𝑗𝐴) → 𝐶𝑊)
6362ralrimiva 3103 . . . 4 (𝜑 → ∀𝑗𝐴 𝐶𝑊)
641mpoexxg 7916 . . . 4 ((𝐴𝑉 ∧ ∀𝑗𝐴 𝐶𝑊) → (𝑗𝐴, 𝑘𝐶𝑋) ∈ V)
6561, 63, 64syl2anc 584 . . 3 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋) ∈ V)
66 gsum2d2.z . . . . 5 0 = (0g𝐺)
6766fvexi 6788 . . . 4 0 ∈ V
6867a1i 11 . . 3 (𝜑0 ∈ V)
69 isfsupp 9132 . . 3 (((𝑗𝐴, 𝑘𝐶𝑋) ∈ V ∧ 0 ∈ V) → ((𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 ↔ (Fun (𝑗𝐴, 𝑘𝐶𝑋) ∧ ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)))
7065, 68, 69syl2anc 584 . 2 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 ↔ (Fun (𝑗𝐴, 𝑘𝐶𝑋) ∧ ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)))
713, 60, 70mpbir2and 710 1 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2106  wral 3064  Vcvv 3432  cdif 3884  {csn 4561  cop 4567   ciun 4924   class class class wbr 5074   × cxp 5587  Rel wrel 5594  Fun wfun 6427  wf 6429  cfv 6433  (class class class)co 7275  cmpo 7277   supp csupp 7977  Fincfn 8733   finSupp cfsupp 9128  Basecbs 16912  0gc0g 17150  CMndccmn 19386
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-1o 8297  df-en 8734  df-fin 8737  df-fsupp 9129
This theorem is referenced by:  gsum2d2  19575  gsumcom2  19576
  Copyright terms: Public domain W3C validator