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

Theorem gsum2d2lem 18758
 Description: Lemma for gsum2d2 18759: 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 2778 . . . 4 (𝑗𝐴, 𝑘𝐶𝑋) = (𝑗𝐴, 𝑘𝐶𝑋)
21mpt2fun 7039 . . 3 Fun (𝑗𝐴, 𝑘𝐶𝑋)
32a1i 11 . 2 (𝜑 → Fun (𝑗𝐴, 𝑘𝐶𝑋))
4 gsum2d2.u . . 3 (𝜑𝑈 ∈ Fin)
5 gsum2d2.f . . . . . 6 ((𝜑 ∧ (𝑗𝐴𝑘𝐶)) → 𝑋𝐵)
65ralrimivva 3153 . . . . 5 (𝜑 → ∀𝑗𝐴𝑘𝐶 𝑋𝐵)
71fmpt2x 7516 . . . . 5 (∀𝑗𝐴𝑘𝐶 𝑋𝐵 ↔ (𝑗𝐴, 𝑘𝐶𝑋): 𝑗𝐴 ({𝑗} × 𝐶)⟶𝐵)
86, 7sylib 210 . . . 4 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋): 𝑗𝐴 ({𝑗} × 𝐶)⟶𝐵)
9 nfv 1957 . . . . . 6 𝑗𝜑
10 nfiu1 4783 . . . . . . . 8 𝑗 𝑗𝐴 ({𝑗} × 𝐶)
11 nfcv 2934 . . . . . . . 8 𝑗𝑈
1210, 11nfdif 3954 . . . . . . 7 𝑗( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
1312nfcri 2929 . . . . . 6 𝑗 𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)
149, 13nfan 1946 . . . . 5 𝑗(𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
15 nfmpt21 6999 . . . . . . 7 𝑗(𝑗𝐴, 𝑘𝐶𝑋)
16 nfcv 2934 . . . . . . 7 𝑗𝑧
1715, 16nffv 6456 . . . . . 6 𝑗((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧)
1817nfeq1 2947 . . . . 5 𝑗((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0
19 relxp 5373 . . . . . . . 8 Rel ({𝑗} × 𝐶)
2019rgenw 3106 . . . . . . 7 𝑗𝐴 Rel ({𝑗} × 𝐶)
21 reliun 5487 . . . . . . 7 (Rel 𝑗𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗𝐴 Rel ({𝑗} × 𝐶))
2220, 21mpbir 223 . . . . . 6 Rel 𝑗𝐴 ({𝑗} × 𝐶)
23 eldifi 3955 . . . . . . 7 (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → 𝑧 𝑗𝐴 ({𝑗} × 𝐶))
2423adantl 475 . . . . . 6 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐶))
25 elrel 5469 . . . . . 6 ((Rel 𝑗𝐴 ({𝑗} × 𝐶) ∧ 𝑧 𝑗𝐴 ({𝑗} × 𝐶)) → ∃𝑗𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
2622, 24, 25sylancr 581 . . . . 5 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ∃𝑗𝑘 𝑧 = ⟨𝑗, 𝑘⟩)
27 nfv 1957 . . . . . 6 𝑘(𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
28 nfmpt22 7000 . . . . . . . 8 𝑘(𝑗𝐴, 𝑘𝐶𝑋)
29 nfcv 2934 . . . . . . . 8 𝑘𝑧
3028, 29nffv 6456 . . . . . . 7 𝑘((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧)
3130nfeq1 2947 . . . . . 6 𝑘((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0
32 simprr 763 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 = ⟨𝑗, 𝑘⟩)
3332fveq2d 6450 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩))
34 df-ov 6925 . . . . . . . . 9 (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩)
35 simprl 761 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
3632, 35eqeltrrd 2860 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈))
3736eldifad 3804 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ⟨𝑗, 𝑘⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐶))
38 opeliunxp 5416 . . . . . . . . . . . 12 (⟨𝑗, 𝑘⟩ ∈ 𝑗𝐴 ({𝑗} × 𝐶) ↔ (𝑗𝐴𝑘𝐶))
3937, 38sylib 210 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗𝐴𝑘𝐶))
4039simpld 490 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑗𝐴)
4139simprd 491 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑘𝐶)
4239, 5syldan 585 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋𝐵)
431ovmpt4g 7060 . . . . . . . . . 10 ((𝑗𝐴𝑘𝐶𝑋𝐵) → (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = 𝑋)
4440, 41, 42, 43syl3anc 1439 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑗(𝑗𝐴, 𝑘𝐶𝑋)𝑘) = 𝑋)
4534, 44syl5eqr 2828 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘⟨𝑗, 𝑘⟩) = 𝑋)
46 eldifn 3956 . . . . . . . . . . . 12 (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) → ¬ 𝑧𝑈)
4746ad2antrl 718 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑧𝑈)
4832eleq1d 2844 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧𝑈 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈))
49 df-br 4887 . . . . . . . . . . . 12 (𝑗𝑈𝑘 ↔ ⟨𝑗, 𝑘⟩ ∈ 𝑈)
5048, 49syl6bbr 281 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → (𝑧𝑈𝑗𝑈𝑘))
5147, 50mtbid 316 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ¬ 𝑗𝑈𝑘)
5239, 51jca 507 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴𝑘𝐶) ∧ ¬ 𝑗𝑈𝑘))
53 gsum2d2.n . . . . . . . . 9 ((𝜑 ∧ ((𝑗𝐴𝑘𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 )
5452, 53syldan 585 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → 𝑋 = 0 )
5533, 45, 543eqtrd 2818 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈) ∧ 𝑧 = ⟨𝑗, 𝑘⟩)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 )
5655expr 450 . . . . . 6 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 ))
5727, 31, 56exlimd 2204 . . . . 5 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → (∃𝑘 𝑧 = ⟨𝑗, 𝑘⟩ → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 ))
5814, 18, 26, 57exlimimdd 2206 . . . 4 ((𝜑𝑧 ∈ ( 𝑗𝐴 ({𝑗} × 𝐶) ∖ 𝑈)) → ((𝑗𝐴, 𝑘𝐶𝑋)‘𝑧) = 0 )
598, 58suppss 7607 . . 3 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ⊆ 𝑈)
60 ssfi 8468 . . 3 ((𝑈 ∈ Fin ∧ ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ⊆ 𝑈) → ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)
614, 59, 60syl2anc 579 . 2 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)
62 gsum2d2.a . . . 4 (𝜑𝐴𝑉)
63 gsum2d2.r . . . . 5 ((𝜑𝑗𝐴) → 𝐶𝑊)
6463ralrimiva 3148 . . . 4 (𝜑 → ∀𝑗𝐴 𝐶𝑊)
651mpt2exxg 7524 . . . 4 ((𝐴𝑉 ∧ ∀𝑗𝐴 𝐶𝑊) → (𝑗𝐴, 𝑘𝐶𝑋) ∈ V)
6662, 64, 65syl2anc 579 . . 3 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋) ∈ V)
67 gsum2d2.z . . . . 5 0 = (0g𝐺)
6867fvexi 6460 . . . 4 0 ∈ V
6968a1i 11 . . 3 (𝜑0 ∈ V)
70 isfsupp 8567 . . 3 (((𝑗𝐴, 𝑘𝐶𝑋) ∈ V ∧ 0 ∈ V) → ((𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 ↔ (Fun (𝑗𝐴, 𝑘𝐶𝑋) ∧ ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)))
7166, 69, 70syl2anc 579 . 2 (𝜑 → ((𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 ↔ (Fun (𝑗𝐴, 𝑘𝐶𝑋) ∧ ((𝑗𝐴, 𝑘𝐶𝑋) supp 0 ) ∈ Fin)))
723, 61, 71mpbir2and 703 1 (𝜑 → (𝑗𝐴, 𝑘𝐶𝑋) finSupp 0 )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601  ∃wex 1823   ∈ wcel 2107  ∀wral 3090  Vcvv 3398   ∖ cdif 3789   ⊆ wss 3792  {csn 4398  ⟨cop 4404  ∪ ciun 4753   class class class wbr 4886   × cxp 5353  Rel wrel 5360  Fun wfun 6129  ⟶wf 6131  ‘cfv 6135  (class class class)co 6922   ↦ cmpt2 6924   supp csupp 7576  Fincfn 8241   finSupp cfsupp 8563  Basecbs 16255  0gc0g 16486  CMndccmn 18579 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-er 8026  df-en 8242  df-fin 8245  df-fsupp 8564 This theorem is referenced by:  gsum2d2  18759  gsumcom2  18760
 Copyright terms: Public domain W3C validator