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

Theorem tsmsxplem1 22165
Description: Lemma for tsmsxp 22167. (Contributed by Mario Carneiro, 21-Sep-2015.)
Hypotheses
Ref Expression
tsmsxp.b 𝐵 = (Base‘𝐺)
tsmsxp.g (𝜑𝐺 ∈ CMnd)
tsmsxp.2 (𝜑𝐺 ∈ TopGrp)
tsmsxp.a (𝜑𝐴𝑉)
tsmsxp.c (𝜑𝐶𝑊)
tsmsxp.f (𝜑𝐹:(𝐴 × 𝐶)⟶𝐵)
tsmsxp.h (𝜑𝐻:𝐴𝐵)
tsmsxp.1 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
tsmsxp.j 𝐽 = (TopOpen‘𝐺)
tsmsxp.z 0 = (0g𝐺)
tsmsxp.p + = (+g𝐺)
tsmsxp.m = (-g𝐺)
tsmsxp.l (𝜑𝐿𝐽)
tsmsxp.3 (𝜑0𝐿)
tsmsxp.k (𝜑𝐾 ∈ (𝒫 𝐴 ∩ Fin))
tsmsxp.ks (𝜑 → dom 𝐷𝐾)
tsmsxp.d (𝜑𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
Assertion
Ref Expression
tsmsxplem1 (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
Distinct variable groups:   0 ,𝑘   𝑗,𝑘,𝑛,𝑥,𝐺   𝐵,𝑘   𝐷,𝑗,𝑘,𝑛,𝑥   𝑗,𝐿,𝑛,𝑥   𝐴,𝑗,𝑘,𝑛   𝑗,𝐾,𝑘,𝑛,𝑥   𝑗,𝐻,𝑘,𝑛,𝑥   ,𝑗,𝑛,𝑥   𝐶,𝑗,𝑘,𝑛   𝑗,𝐹,𝑘,𝑛,𝑥   𝜑,𝑗,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐵(𝑥,𝑗,𝑛)   𝐶(𝑥)   + (𝑥,𝑗,𝑘,𝑛)   𝐽(𝑥,𝑗,𝑘,𝑛)   𝐿(𝑘)   (𝑘)   𝑉(𝑥,𝑗,𝑘,𝑛)   𝑊(𝑥,𝑗,𝑘,𝑛)   0 (𝑥,𝑗,𝑛)

Proof of Theorem tsmsxplem1
Dummy variables 𝑔 𝑦 𝑧 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsxp.k . . . 4 (𝜑𝐾 ∈ (𝒫 𝐴 ∩ Fin))
2 elfpw 8503 . . . . 5 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾𝐴𝐾 ∈ Fin))
32simprbi 486 . . . 4 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ∈ Fin)
41, 3syl 17 . . 3 (𝜑𝐾 ∈ Fin)
52simplbi 487 . . . . . . 7 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾𝐴)
61, 5syl 17 . . . . . 6 (𝜑𝐾𝐴)
76sselda 3798 . . . . 5 ((𝜑𝑗𝐾) → 𝑗𝐴)
8 tsmsxp.b . . . . . 6 𝐵 = (Base‘𝐺)
9 tsmsxp.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
10 eqid 2806 . . . . . 6 (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
11 tsmsxp.g . . . . . . 7 (𝜑𝐺 ∈ CMnd)
1211adantr 468 . . . . . 6 ((𝜑𝑗𝐴) → 𝐺 ∈ CMnd)
13 tsmsxp.2 . . . . . . . 8 (𝜑𝐺 ∈ TopGrp)
14 tgptps 22093 . . . . . . . 8 (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
1513, 14syl 17 . . . . . . 7 (𝜑𝐺 ∈ TopSp)
1615adantr 468 . . . . . 6 ((𝜑𝑗𝐴) → 𝐺 ∈ TopSp)
17 tsmsxp.c . . . . . . 7 (𝜑𝐶𝑊)
1817adantr 468 . . . . . 6 ((𝜑𝑗𝐴) → 𝐶𝑊)
19 tsmsxp.f . . . . . . . . 9 (𝜑𝐹:(𝐴 × 𝐶)⟶𝐵)
20 fovrn 7030 . . . . . . . . 9 ((𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
2119, 20syl3an1 1195 . . . . . . . 8 ((𝜑𝑗𝐴𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
22213expa 1140 . . . . . . 7 (((𝜑𝑗𝐴) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
2322fmpttd 6603 . . . . . 6 ((𝜑𝑗𝐴) → (𝑘𝐶 ↦ (𝑗𝐹𝑘)):𝐶𝐵)
24 tsmsxp.1 . . . . . 6 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
25 df-ima 5324 . . . . . . . 8 ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) = ran ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿)
269, 8tgptopon 22095 . . . . . . . . . . . . 13 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
2713, 26syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ (TopOn‘𝐵))
28 tsmsxp.l . . . . . . . . . . . 12 (𝜑𝐿𝐽)
29 toponss 20941 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿𝐽) → 𝐿𝐵)
3027, 28, 29syl2anc 575 . . . . . . . . . . 11 (𝜑𝐿𝐵)
3130adantr 468 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐿𝐵)
3231resmptd 5657 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿) = (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
3332rneqd 5554 . . . . . . . 8 ((𝜑𝑗𝐴) → ran ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿) = ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
3425, 33syl5eq 2852 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) = ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
35 tsmsxp.h . . . . . . . . . . . . 13 (𝜑𝐻:𝐴𝐵)
3635ffvelrnda 6577 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ 𝐵)
37 tsmsxp.p . . . . . . . . . . . . 13 + = (+g𝐺)
38 eqid 2806 . . . . . . . . . . . . 13 (invg𝐺) = (invg𝐺)
39 tsmsxp.m . . . . . . . . . . . . 13 = (-g𝐺)
408, 37, 38, 39grpsubval 17666 . . . . . . . . . . . 12 (((𝐻𝑗) ∈ 𝐵𝑔𝐵) → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
4136, 40sylan 571 . . . . . . . . . . 11 (((𝜑𝑗𝐴) ∧ 𝑔𝐵) → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
4241mpteq2dva 4938 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) = (𝑔𝐵 ↦ ((𝐻𝑗) + ((invg𝐺)‘𝑔))))
43 tgpgrp 22091 . . . . . . . . . . . . . 14 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
4413, 43syl 17 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ Grp)
4544adantr 468 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → 𝐺 ∈ Grp)
468, 38grpinvcl 17668 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑔𝐵) → ((invg𝐺)‘𝑔) ∈ 𝐵)
4745, 46sylan 571 . . . . . . . . . . 11 (((𝜑𝑗𝐴) ∧ 𝑔𝐵) → ((invg𝐺)‘𝑔) ∈ 𝐵)
488, 38grpinvf 17667 . . . . . . . . . . . . 13 (𝐺 ∈ Grp → (invg𝐺):𝐵𝐵)
4945, 48syl 17 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → (invg𝐺):𝐵𝐵)
5049feqmptd 6466 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → (invg𝐺) = (𝑔𝐵 ↦ ((invg𝐺)‘𝑔)))
51 eqidd 2807 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) = (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)))
52 oveq2 6878 . . . . . . . . . . 11 (𝑦 = ((invg𝐺)‘𝑔) → ((𝐻𝑗) + 𝑦) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
5347, 50, 51, 52fmptco 6615 . . . . . . . . . 10 ((𝜑𝑗𝐴) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) = (𝑔𝐵 ↦ ((𝐻𝑗) + ((invg𝐺)‘𝑔))))
5442, 53eqtr4d 2843 . . . . . . . . 9 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) = ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)))
5513adantr 468 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → 𝐺 ∈ TopGrp)
569, 38grpinvhmeo 22099 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → (invg𝐺) ∈ (𝐽Homeo𝐽))
5755, 56syl 17 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (invg𝐺) ∈ (𝐽Homeo𝐽))
58 eqid 2806 . . . . . . . . . . . 12 (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) = (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦))
5958, 8, 37, 9tgplacthmeo 22116 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ (𝐻𝑗) ∈ 𝐵) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
6055, 36, 59syl2anc 575 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
61 hmeoco 21785 . . . . . . . . . 10 (((invg𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6257, 60, 61syl2anc 575 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6354, 62eqeltrd 2885 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ∈ (𝐽Homeo𝐽))
6428adantr 468 . . . . . . . 8 ((𝜑𝑗𝐴) → 𝐿𝐽)
65 hmeoima 21778 . . . . . . . 8 (((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿𝐽) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) ∈ 𝐽)
6663, 64, 65syl2anc 575 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) ∈ 𝐽)
6734, 66eqeltrrd 2886 . . . . . 6 ((𝜑𝑗𝐴) → ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ∈ 𝐽)
68 tsmsxp.z . . . . . . . . 9 0 = (0g𝐺)
698, 68, 39grpsubid1 17701 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝐻𝑗) ∈ 𝐵) → ((𝐻𝑗) 0 ) = (𝐻𝑗))
7045, 36, 69syl2anc 575 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐻𝑗) 0 ) = (𝐻𝑗))
71 tsmsxp.3 . . . . . . . . 9 (𝜑0𝐿)
7271adantr 468 . . . . . . . 8 ((𝜑𝑗𝐴) → 0𝐿)
73 ovex 6902 . . . . . . . 8 ((𝐻𝑗) 0 ) ∈ V
74 eqid 2806 . . . . . . . . 9 (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) = (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))
75 oveq2 6878 . . . . . . . . 9 (𝑔 = 0 → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) 0 ))
7674, 75elrnmpt1s 5574 . . . . . . . 8 (( 0𝐿 ∧ ((𝐻𝑗) 0 ) ∈ V) → ((𝐻𝑗) 0 ) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
7772, 73, 76sylancl 576 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐻𝑗) 0 ) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
7870, 77eqeltrrd 2886 . . . . . 6 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
798, 9, 10, 12, 16, 18, 23, 24, 67, 78tsmsi 22146 . . . . 5 ((𝜑𝑗𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
807, 79syldan 581 . . . 4 ((𝜑𝑗𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
8180ralrimiva 3154 . . 3 (𝜑 → ∀𝑗𝐾𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
82 sseq1 3823 . . . . . 6 (𝑦 = (𝑓𝑗) → (𝑦𝑧 ↔ (𝑓𝑗) ⊆ 𝑧))
8382imbi1d 332 . . . . 5 (𝑦 = (𝑓𝑗) → ((𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ ((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
8483ralbidv 3174 . . . 4 (𝑦 = (𝑓𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
8584ac6sfi 8439 . . 3 ((𝐾 ∈ Fin ∧ ∀𝑗𝐾𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
864, 81, 85syl2anc 575 . 2 (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
87 frn 6258 . . . . . . . . 9 (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
8887adantl 469 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
89 inss1 4029 . . . . . . . 8 (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
9088, 89syl6ss 3810 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
91 sspwuni 4803 . . . . . . 7 (ran 𝑓 ⊆ 𝒫 𝐶 ran 𝑓𝐶)
9290, 91sylib 209 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓𝐶)
93 tsmsxp.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
94 elfpw 8503 . . . . . . . . . 10 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
9594simplbi 487 . . . . . . . . 9 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
96 rnss 5555 . . . . . . . . 9 (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
9793, 95, 963syl 18 . . . . . . . 8 (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
98 rnxpss 5777 . . . . . . . 8 ran (𝐴 × 𝐶) ⊆ 𝐶
9997, 98syl6ss 3810 . . . . . . 7 (𝜑 → ran 𝐷𝐶)
10099adantr 468 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷𝐶)
10192, 100unssd 3988 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
1024adantr 468 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
103 ffn 6252 . . . . . . . . . 10 (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
104103adantl 469 . . . . . . . . 9 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
105 dffn4 6333 . . . . . . . . 9 (𝑓 Fn 𝐾𝑓:𝐾onto→ran 𝑓)
106104, 105sylib 209 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾onto→ran 𝑓)
107 fofi 8487 . . . . . . . 8 ((𝐾 ∈ Fin ∧ 𝑓:𝐾onto→ran 𝑓) → ran 𝑓 ∈ Fin)
108102, 106, 107syl2anc 575 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
109 inss2 4030 . . . . . . . 8 (𝒫 𝐶 ∩ Fin) ⊆ Fin
11088, 109syl6ss 3810 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
111 unifi 8490 . . . . . . 7 ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ran 𝑓 ∈ Fin)
112108, 110, 111syl2anc 575 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
11394simprbi 486 . . . . . . . 8 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
114 rnfi 8484 . . . . . . . 8 (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
11593, 113, 1143syl 18 . . . . . . 7 (𝜑 → ran 𝐷 ∈ Fin)
116115adantr 468 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
117 unfi 8462 . . . . . 6 (( ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
118112, 116, 117syl2anc 575 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
119 elfpw 8503 . . . . 5 (( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ (( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ ( ran 𝑓 ∪ ran 𝐷) ∈ Fin))
120101, 118, 119sylanbrc 574 . . . 4 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
121120adantrr 699 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
122 ssun2 3976 . . . 4 ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷)
123122a1i 11 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷))
124120adantlr 697 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
125 fvssunirn 6433 . . . . . . . . . . . . . 14 (𝑓𝑗) ⊆ ran 𝑓
126 ssun1 3975 . . . . . . . . . . . . . 14 ran 𝑓 ⊆ ( ran 𝑓 ∪ ran 𝐷)
127125, 126sstri 3807 . . . . . . . . . . . . 13 (𝑓𝑗) ⊆ ( ran 𝑓 ∪ ran 𝐷)
128 id 22 . . . . . . . . . . . . 13 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → 𝑧 = ( ran 𝑓 ∪ ran 𝐷))
129127, 128syl5sseqr 3851 . . . . . . . . . . . 12 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (𝑓𝑗) ⊆ 𝑧)
130 pm5.5 352 . . . . . . . . . . . 12 ((𝑓𝑗) ⊆ 𝑧 → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
131129, 130syl 17 . . . . . . . . . . 11 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
132 reseq2 5592 . . . . . . . . . . . . 13 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷)))
133132oveq2d 6886 . . . . . . . . . . . 12 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))))
134133eleq1d 2870 . . . . . . . . . . 11 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
135131, 134bitrd 270 . . . . . . . . . 10 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
136135rspcv 3498 . . . . . . . . 9 (( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
137124, 136syl 17 . . . . . . . 8 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
13811ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
139 cmnmnd 18405 . . . . . . . . . . . . 13 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
140138, 139syl 17 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
141 simplr 776 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗𝐾)
142118adantlr 697 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
143101adantlr 697 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
144143sselda 3798 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → 𝑘𝐶)
14519adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
146145, 7jca 503 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴))
147203expa 1140 . . . . . . . . . . . . . . . . 17 (((𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
148146, 147sylan 571 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐾) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149148adantlr 697 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
150144, 149syldan 581 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
151150fmpttd 6603 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):( ran 𝑓 ∪ ran 𝐷)⟶𝐵)
152 eqid 2806 . . . . . . . . . . . . . 14 (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
153 ovexd 6904 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
15468fvexi 6418 . . . . . . . . . . . . . . 15 0 ∈ V
155154a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
156152, 142, 153, 155fsuppmptdm 8521 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
1578, 68, 138, 142, 151, 156gsumcl 18513 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
158 velsn 4386 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
159 ovres 7026 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
160158, 159sylanbr 573 . . . . . . . . . . . . . . . 16 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
161 oveq1 6877 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
162161adantr 468 . . . . . . . . . . . . . . . 16 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
163160, 162eqtrd 2840 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
164163mpteq2dva 4938 . . . . . . . . . . . . . 14 (𝑦 = 𝑗 → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
165164oveq2d 6886 . . . . . . . . . . . . 13 (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
1668, 165gsumsn 18551 . . . . . . . . . . . 12 ((𝐺 ∈ Mnd ∧ 𝑗𝐾 ∧ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
167140, 141, 157, 166syl3anc 1483 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
168 snfi 8273 . . . . . . . . . . . . 13 {𝑗} ∈ Fin
169168a1i 11 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
17019ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
1717adantr 468 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗𝐴)
172171snssd 4530 . . . . . . . . . . . . . 14 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
173 xpss12 5326 . . . . . . . . . . . . . 14 (({𝑗} ⊆ 𝐴 ∧ ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
174172, 143, 173syl2anc 575 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
175170, 174fssresd 6282 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))):({𝑗} × ( ran 𝑓 ∪ ran 𝐷))⟶𝐵)
176 xpfi 8466 . . . . . . . . . . . . . 14 (({𝑗} ∈ Fin ∧ ( ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
177168, 142, 176sylancr 577 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
178175, 177, 155fdmfifsupp 8520 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
1798, 68, 138, 169, 142, 175, 178gsumxp 18572 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))))
180143resmptd 5657 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
181180oveq2d 6886 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
182167, 179, 1813eqtr4rd 2851 . . . . . . . . . 10 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))))
183182eleq1d 2870 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
184 ovex 6902 . . . . . . . . . . 11 ((𝐻𝑗) 𝑔) ∈ V
18574, 184elrnmpti 5577 . . . . . . . . . 10 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ ∃𝑔𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔))
186 isabl 18394 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
18744, 11, 186sylanbrc 574 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ Abel)
188187ad3antrrr 712 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝐺 ∈ Abel)
1897, 36syldan 581 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝐾) → (𝐻𝑗) ∈ 𝐵)
190189ad2antrr 708 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → (𝐻𝑗) ∈ 𝐵)
19130ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿𝐵)
192191sselda 3798 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝑔𝐵)
1938, 39, 188, 190, 192ablnncan 18423 . . . . . . . . . . . . 13 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐻𝑗) ((𝐻𝑗) 𝑔)) = 𝑔)
194 simpr 473 . . . . . . . . . . . . 13 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝑔𝐿)
195193, 194eqeltrd 2885 . . . . . . . . . . . 12 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐻𝑗) ((𝐻𝑗) 𝑔)) ∈ 𝐿)
196 oveq2 6878 . . . . . . . . . . . . 13 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) = ((𝐻𝑗) ((𝐻𝑗) 𝑔)))
197196eleq1d 2870 . . . . . . . . . . . 12 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → (((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻𝑗) ((𝐻𝑗) 𝑔)) ∈ 𝐿))
198195, 197syl5ibrcom 238 . . . . . . . . . . 11 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
199198rexlimdva 3219 . . . . . . . . . 10 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
200185, 199syl5bi 233 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
201183, 200sylbid 231 . . . . . . . 8 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
202137, 201syld 47 . . . . . . 7 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203202an32s 634 . . . . . 6 (((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204203ralimdva 3150 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
205204impr 444 . . . 4 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
206 fveq2 6404 . . . . . . 7 (𝑗 = 𝑥 → (𝐻𝑗) = (𝐻𝑥))
207 sneq 4380 . . . . . . . . . 10 (𝑗 = 𝑥 → {𝑗} = {𝑥})
208207xpeq1d 5339 . . . . . . . . 9 (𝑗 = 𝑥 → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))
209208reseq2d 5597 . . . . . . . 8 (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))
210209oveq2d 6886 . . . . . . 7 (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))))
211206, 210oveq12d 6888 . . . . . 6 (𝑗 = 𝑥 → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) = ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))))
212211eleq1d 2870 . . . . 5 (𝑗 = 𝑥 → (((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
213212cbvralv 3360 . . . 4 (∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
214205, 213sylib 209 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
215 sseq2 3824 . . . . 5 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (ran 𝐷𝑛 ↔ ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷)))
216 xpeq2 5331 . . . . . . . . . 10 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))
217216reseq2d 5597 . . . . . . . . 9 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))
218217oveq2d 6886 . . . . . . . 8 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))))
219218oveq2d 6886 . . . . . . 7 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))))
220219eleq1d 2870 . . . . . 6 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
221220ralbidv 3174 . . . . 5 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
222215, 221anbi12d 618 . . . 4 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)))
223222rspcev 3502 . . 3 ((( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
224121, 123, 214, 223syl12anc 856 . 2 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
22586, 224exlimddv 2026 1 (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2156  wral 3096  wrex 3097  Vcvv 3391  cun 3767  cin 3768  wss 3769  𝒫 cpw 4351  {csn 4370   cuni 4630  cmpt 4923   × cxp 5309  dom cdm 5311  ran crn 5312  cres 5313  cima 5314  ccom 5315   Fn wfn 6092  wf 6093  ontowfo 6095  cfv 6097  (class class class)co 6870  Fincfn 8188  Basecbs 16064  +gcplusg 16149  TopOpenctopn 16283  0gc0g 16301   Σg cgsu 16302  Mndcmnd 17495  Grpcgrp 17623  invgcminusg 17624  -gcsg 17625  CMndccmn 18390  Abelcabl 18391  TopOnctopon 20924  TopSpctps 20946  Homeochmeo 21766  TopGrpctgp 22084   tsums ctsu 22138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-of 7123  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-oadd 7796  df-er 7975  df-map 8090  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-fsupp 8511  df-oi 8650  df-card 9044  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-nn 11302  df-2 11360  df-n0 11556  df-z 11640  df-uz 11901  df-fz 12546  df-fzo 12686  df-seq 13021  df-hash 13334  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-0g 16303  df-gsum 16304  df-topgen 16305  df-mre 16447  df-mrc 16448  df-acs 16450  df-plusf 17442  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-cntz 17947  df-cmn 18392  df-abl 18393  df-fbas 19947  df-fg 19948  df-top 20908  df-topon 20925  df-topsp 20947  df-bases 20960  df-ntr 21034  df-nei 21112  df-cn 21241  df-cnp 21242  df-tx 21575  df-hmeo 21768  df-fil 21859  df-fm 21951  df-flim 21952  df-flf 21953  df-tmd 22085  df-tgp 22086  df-tsms 22139
This theorem is referenced by:  tsmsxp  22167
  Copyright terms: Public domain W3C validator