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

Theorem tsmsxplem1 21866
 Description: Lemma for tsmsxp 21868. (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 8212 . . . . 5 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾𝐴𝐾 ∈ Fin))
32simprbi 480 . . . 4 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ∈ Fin)
41, 3syl 17 . . 3 (𝜑𝐾 ∈ Fin)
52simplbi 476 . . . . . . 7 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾𝐴)
61, 5syl 17 . . . . . 6 (𝜑𝐾𝐴)
76sselda 3583 . . . . 5 ((𝜑𝑗𝐾) → 𝑗𝐴)
8 tsmsxp.b . . . . . 6 𝐵 = (Base‘𝐺)
9 tsmsxp.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
10 eqid 2621 . . . . . 6 (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
11 tsmsxp.g . . . . . . 7 (𝜑𝐺 ∈ CMnd)
1211adantr 481 . . . . . 6 ((𝜑𝑗𝐴) → 𝐺 ∈ CMnd)
13 tsmsxp.2 . . . . . . . 8 (𝜑𝐺 ∈ TopGrp)
14 tgptps 21794 . . . . . . . 8 (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
1513, 14syl 17 . . . . . . 7 (𝜑𝐺 ∈ TopSp)
1615adantr 481 . . . . . 6 ((𝜑𝑗𝐴) → 𝐺 ∈ TopSp)
17 tsmsxp.c . . . . . . 7 (𝜑𝐶𝑊)
1817adantr 481 . . . . . 6 ((𝜑𝑗𝐴) → 𝐶𝑊)
19 tsmsxp.f . . . . . . . . 9 (𝜑𝐹:(𝐴 × 𝐶)⟶𝐵)
20 fovrn 6757 . . . . . . . . 9 ((𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
2119, 20syl3an1 1356 . . . . . . . 8 ((𝜑𝑗𝐴𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
22213expa 1262 . . . . . . 7 (((𝜑𝑗𝐴) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
23 eqid 2621 . . . . . . 7 (𝑘𝐶 ↦ (𝑗𝐹𝑘)) = (𝑘𝐶 ↦ (𝑗𝐹𝑘))
2422, 23fmptd 6340 . . . . . 6 ((𝜑𝑗𝐴) → (𝑘𝐶 ↦ (𝑗𝐹𝑘)):𝐶𝐵)
25 tsmsxp.1 . . . . . 6 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
26 df-ima 5087 . . . . . . . 8 ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) = ran ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿)
279, 8tgptopon 21796 . . . . . . . . . . . . 13 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
2813, 27syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ (TopOn‘𝐵))
29 tsmsxp.l . . . . . . . . . . . 12 (𝜑𝐿𝐽)
30 toponss 20644 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿𝐽) → 𝐿𝐵)
3128, 29, 30syl2anc 692 . . . . . . . . . . 11 (𝜑𝐿𝐵)
3231adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐿𝐵)
3332resmptd 5411 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿) = (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
3433rneqd 5313 . . . . . . . 8 ((𝜑𝑗𝐴) → ran ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿) = ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
3526, 34syl5eq 2667 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) = ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
36 tsmsxp.h . . . . . . . . . . . . 13 (𝜑𝐻:𝐴𝐵)
3736ffvelrnda 6315 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ 𝐵)
38 tsmsxp.p . . . . . . . . . . . . 13 + = (+g𝐺)
39 eqid 2621 . . . . . . . . . . . . 13 (invg𝐺) = (invg𝐺)
40 tsmsxp.m . . . . . . . . . . . . 13 = (-g𝐺)
418, 38, 39, 40grpsubval 17386 . . . . . . . . . . . 12 (((𝐻𝑗) ∈ 𝐵𝑔𝐵) → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
4237, 41sylan 488 . . . . . . . . . . 11 (((𝜑𝑗𝐴) ∧ 𝑔𝐵) → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
4342mpteq2dva 4704 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) = (𝑔𝐵 ↦ ((𝐻𝑗) + ((invg𝐺)‘𝑔))))
44 tgpgrp 21792 . . . . . . . . . . . . . 14 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
4513, 44syl 17 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ Grp)
4645adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → 𝐺 ∈ Grp)
478, 39grpinvcl 17388 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑔𝐵) → ((invg𝐺)‘𝑔) ∈ 𝐵)
4846, 47sylan 488 . . . . . . . . . . 11 (((𝜑𝑗𝐴) ∧ 𝑔𝐵) → ((invg𝐺)‘𝑔) ∈ 𝐵)
498, 39grpinvf 17387 . . . . . . . . . . . . 13 (𝐺 ∈ Grp → (invg𝐺):𝐵𝐵)
5046, 49syl 17 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → (invg𝐺):𝐵𝐵)
5150feqmptd 6206 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → (invg𝐺) = (𝑔𝐵 ↦ ((invg𝐺)‘𝑔)))
52 eqidd 2622 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) = (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)))
53 oveq2 6612 . . . . . . . . . . 11 (𝑦 = ((invg𝐺)‘𝑔) → ((𝐻𝑗) + 𝑦) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
5448, 51, 52, 53fmptco 6351 . . . . . . . . . 10 ((𝜑𝑗𝐴) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) = (𝑔𝐵 ↦ ((𝐻𝑗) + ((invg𝐺)‘𝑔))))
5543, 54eqtr4d 2658 . . . . . . . . 9 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) = ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)))
5613adantr 481 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → 𝐺 ∈ TopGrp)
579, 39grpinvhmeo 21800 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → (invg𝐺) ∈ (𝐽Homeo𝐽))
5856, 57syl 17 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (invg𝐺) ∈ (𝐽Homeo𝐽))
59 eqid 2621 . . . . . . . . . . . 12 (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) = (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦))
6059, 8, 38, 9tgplacthmeo 21817 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ (𝐻𝑗) ∈ 𝐵) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
6156, 37, 60syl2anc 692 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
62 hmeoco 21485 . . . . . . . . . 10 (((invg𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6358, 61, 62syl2anc 692 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6455, 63eqeltrd 2698 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ∈ (𝐽Homeo𝐽))
6529adantr 481 . . . . . . . 8 ((𝜑𝑗𝐴) → 𝐿𝐽)
66 hmeoima 21478 . . . . . . . 8 (((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿𝐽) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) ∈ 𝐽)
6764, 65, 66syl2anc 692 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) ∈ 𝐽)
6835, 67eqeltrrd 2699 . . . . . 6 ((𝜑𝑗𝐴) → ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ∈ 𝐽)
69 tsmsxp.z . . . . . . . . 9 0 = (0g𝐺)
708, 69, 40grpsubid1 17421 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝐻𝑗) ∈ 𝐵) → ((𝐻𝑗) 0 ) = (𝐻𝑗))
7146, 37, 70syl2anc 692 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐻𝑗) 0 ) = (𝐻𝑗))
72 tsmsxp.3 . . . . . . . . 9 (𝜑0𝐿)
7372adantr 481 . . . . . . . 8 ((𝜑𝑗𝐴) → 0𝐿)
74 ovex 6632 . . . . . . . 8 ((𝐻𝑗) 0 ) ∈ V
75 eqid 2621 . . . . . . . . 9 (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) = (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))
76 oveq2 6612 . . . . . . . . 9 (𝑔 = 0 → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) 0 ))
7775, 76elrnmpt1s 5333 . . . . . . . 8 (( 0𝐿 ∧ ((𝐻𝑗) 0 ) ∈ V) → ((𝐻𝑗) 0 ) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
7873, 74, 77sylancl 693 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐻𝑗) 0 ) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
7971, 78eqeltrrd 2699 . . . . . 6 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
808, 9, 10, 12, 16, 18, 24, 25, 68, 79tsmsi 21847 . . . . 5 ((𝜑𝑗𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
817, 80syldan 487 . . . 4 ((𝜑𝑗𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
8281ralrimiva 2960 . . 3 (𝜑 → ∀𝑗𝐾𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
83 sseq1 3605 . . . . . 6 (𝑦 = (𝑓𝑗) → (𝑦𝑧 ↔ (𝑓𝑗) ⊆ 𝑧))
8483imbi1d 331 . . . . 5 (𝑦 = (𝑓𝑗) → ((𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ ((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
8584ralbidv 2980 . . . 4 (𝑦 = (𝑓𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
8685ac6sfi 8148 . . 3 ((𝐾 ∈ Fin ∧ ∀𝑗𝐾𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
874, 82, 86syl2anc 692 . 2 (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
88 frn 6010 . . . . . . . . 9 (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
8988adantl 482 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
90 inss1 3811 . . . . . . . 8 (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
9189, 90syl6ss 3595 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
92 sspwuni 4577 . . . . . . 7 (ran 𝑓 ⊆ 𝒫 𝐶 ran 𝑓𝐶)
9391, 92sylib 208 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓𝐶)
94 tsmsxp.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
95 elfpw 8212 . . . . . . . . . 10 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
9695simplbi 476 . . . . . . . . 9 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
97 rnss 5314 . . . . . . . . 9 (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
9894, 96, 973syl 18 . . . . . . . 8 (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
99 rnxpss 5525 . . . . . . . 8 ran (𝐴 × 𝐶) ⊆ 𝐶
10098, 99syl6ss 3595 . . . . . . 7 (𝜑 → ran 𝐷𝐶)
101100adantr 481 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷𝐶)
10293, 101unssd 3767 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
1034adantr 481 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
104 ffn 6002 . . . . . . . . . 10 (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
105104adantl 482 . . . . . . . . 9 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
106 dffn4 6078 . . . . . . . . 9 (𝑓 Fn 𝐾𝑓:𝐾onto→ran 𝑓)
107105, 106sylib 208 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾onto→ran 𝑓)
108 fofi 8196 . . . . . . . 8 ((𝐾 ∈ Fin ∧ 𝑓:𝐾onto→ran 𝑓) → ran 𝑓 ∈ Fin)
109103, 107, 108syl2anc 692 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
110 inss2 3812 . . . . . . . 8 (𝒫 𝐶 ∩ Fin) ⊆ Fin
11189, 110syl6ss 3595 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
112 unifi 8199 . . . . . . 7 ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ran 𝑓 ∈ Fin)
113109, 111, 112syl2anc 692 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
11495simprbi 480 . . . . . . . 8 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
115 rnfi 8193 . . . . . . . 8 (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
11694, 114, 1153syl 18 . . . . . . 7 (𝜑 → ran 𝐷 ∈ Fin)
117116adantr 481 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
118 unfi 8171 . . . . . 6 (( ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
119113, 117, 118syl2anc 692 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
120 elfpw 8212 . . . . 5 (( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ (( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ ( ran 𝑓 ∪ ran 𝐷) ∈ Fin))
121102, 119, 120sylanbrc 697 . . . 4 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
122121adantrr 752 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
123 ssun2 3755 . . . 4 ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷)
124123a1i 11 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷))
125121adantlr 750 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
126 fvssunirn 6174 . . . . . . . . . . . . . 14 (𝑓𝑗) ⊆ ran 𝑓
127 ssun1 3754 . . . . . . . . . . . . . 14 ran 𝑓 ⊆ ( ran 𝑓 ∪ ran 𝐷)
128126, 127sstri 3592 . . . . . . . . . . . . 13 (𝑓𝑗) ⊆ ( ran 𝑓 ∪ ran 𝐷)
129 id 22 . . . . . . . . . . . . 13 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → 𝑧 = ( ran 𝑓 ∪ ran 𝐷))
130128, 129syl5sseqr 3633 . . . . . . . . . . . 12 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (𝑓𝑗) ⊆ 𝑧)
131 pm5.5 351 . . . . . . . . . . . 12 ((𝑓𝑗) ⊆ 𝑧 → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
132130, 131syl 17 . . . . . . . . . . 11 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
133 reseq2 5351 . . . . . . . . . . . . 13 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷)))
134133oveq2d 6620 . . . . . . . . . . . 12 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))))
135134eleq1d 2683 . . . . . . . . . . 11 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
136132, 135bitrd 268 . . . . . . . . . 10 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
137136rspcv 3291 . . . . . . . . 9 (( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
138125, 137syl 17 . . . . . . . 8 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
13911ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
140 cmnmnd 18129 . . . . . . . . . . . . 13 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
141139, 140syl 17 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
142 simplr 791 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗𝐾)
143119adantlr 750 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
144102adantlr 750 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
145144sselda 3583 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → 𝑘𝐶)
14619adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
147146, 7jca 554 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴))
148203expa 1262 . . . . . . . . . . . . . . . . 17 (((𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149147, 148sylan 488 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐾) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
150149adantlr 750 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
151145, 150syldan 487 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
152 eqid 2621 . . . . . . . . . . . . . 14 (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
153151, 152fmptd 6340 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):( ran 𝑓 ∪ ran 𝐷)⟶𝐵)
154 ovex 6632 . . . . . . . . . . . . . . 15 (𝑗𝐹𝑘) ∈ V
155154a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
156 fvex 6158 . . . . . . . . . . . . . . . 16 (0g𝐺) ∈ V
15769, 156eqeltri 2694 . . . . . . . . . . . . . . 15 0 ∈ V
158157a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
159152, 143, 155, 158fsuppmptdm 8230 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
1608, 69, 139, 143, 153, 159gsumcl 18237 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
161 velsn 4164 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
162 ovres 6753 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
163161, 162sylanbr 490 . . . . . . . . . . . . . . . 16 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
164 oveq1 6611 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
165164adantr 481 . . . . . . . . . . . . . . . 16 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
166163, 165eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
167166mpteq2dva 4704 . . . . . . . . . . . . . 14 (𝑦 = 𝑗 → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
168167oveq2d 6620 . . . . . . . . . . . . 13 (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
1698, 168gsumsn 18275 . . . . . . . . . . . 12 ((𝐺 ∈ Mnd ∧ 𝑗𝐾 ∧ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
170141, 142, 160, 169syl3anc 1323 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
171 snfi 7982 . . . . . . . . . . . . 13 {𝑗} ∈ Fin
172171a1i 11 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
17319ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
1747adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗𝐴)
175174snssd 4309 . . . . . . . . . . . . . 14 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
176 xpss12 5186 . . . . . . . . . . . . . 14 (({𝑗} ⊆ 𝐴 ∧ ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
177175, 144, 176syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
178173, 177fssresd 6028 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))):({𝑗} × ( ran 𝑓 ∪ ran 𝐷))⟶𝐵)
179 xpfi 8175 . . . . . . . . . . . . . 14 (({𝑗} ∈ Fin ∧ ( ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
180171, 143, 179sylancr 694 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
181178, 180, 158fdmfifsupp 8229 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
1828, 69, 139, 172, 143, 178, 181gsumxp 18296 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))))
183144resmptd 5411 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
184183oveq2d 6620 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
185170, 182, 1843eqtr4rd 2666 . . . . . . . . . 10 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))))
186185eleq1d 2683 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
187 ovex 6632 . . . . . . . . . . 11 ((𝐻𝑗) 𝑔) ∈ V
18875, 187elrnmpti 5336 . . . . . . . . . 10 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ ∃𝑔𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔))
189 isabl 18118 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
19045, 11, 189sylanbrc 697 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ Abel)
191190ad3antrrr 765 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝐺 ∈ Abel)
1927, 37syldan 487 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝐾) → (𝐻𝑗) ∈ 𝐵)
193192ad2antrr 761 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → (𝐻𝑗) ∈ 𝐵)
19431ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿𝐵)
195194sselda 3583 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝑔𝐵)
1968, 40, 191, 193, 195ablnncan 18147 . . . . . . . . . . . . 13 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐻𝑗) ((𝐻𝑗) 𝑔)) = 𝑔)
197 simpr 477 . . . . . . . . . . . . 13 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝑔𝐿)
198196, 197eqeltrd 2698 . . . . . . . . . . . 12 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐻𝑗) ((𝐻𝑗) 𝑔)) ∈ 𝐿)
199 oveq2 6612 . . . . . . . . . . . . 13 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) = ((𝐻𝑗) ((𝐻𝑗) 𝑔)))
200199eleq1d 2683 . . . . . . . . . . . 12 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → (((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻𝑗) ((𝐻𝑗) 𝑔)) ∈ 𝐿))
201198, 200syl5ibrcom 237 . . . . . . . . . . 11 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
202201rexlimdva 3024 . . . . . . . . . 10 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203188, 202syl5bi 232 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204186, 203sylbid 230 . . . . . . . 8 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
205138, 204syld 47 . . . . . . 7 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
206205an32s 845 . . . . . 6 (((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
207206ralimdva 2956 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
208207impr 648 . . . 4 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
209 fveq2 6148 . . . . . . 7 (𝑗 = 𝑥 → (𝐻𝑗) = (𝐻𝑥))
210 sneq 4158 . . . . . . . . . 10 (𝑗 = 𝑥 → {𝑗} = {𝑥})
211210xpeq1d 5098 . . . . . . . . 9 (𝑗 = 𝑥 → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))
212211reseq2d 5356 . . . . . . . 8 (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))
213212oveq2d 6620 . . . . . . 7 (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))))
214209, 213oveq12d 6622 . . . . . 6 (𝑗 = 𝑥 → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) = ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))))
215214eleq1d 2683 . . . . 5 (𝑗 = 𝑥 → (((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
216215cbvralv 3159 . . . 4 (∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
217208, 216sylib 208 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
218 sseq2 3606 . . . . 5 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (ran 𝐷𝑛 ↔ ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷)))
219 xpeq2 5089 . . . . . . . . . 10 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))
220219reseq2d 5356 . . . . . . . . 9 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))
221220oveq2d 6620 . . . . . . . 8 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))))
222221oveq2d 6620 . . . . . . 7 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))))
223222eleq1d 2683 . . . . . 6 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
224223ralbidv 2980 . . . . 5 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
225218, 224anbi12d 746 . . . 4 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)))
226225rspcev 3295 . . 3 ((( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
227122, 124, 217, 226syl12anc 1321 . 2 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
22887, 227exlimddv 1860 1 (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∪ cun 3553   ∩ cin 3554   ⊆ wss 3555  𝒫 cpw 4130  {csn 4148  ∪ cuni 4402   ↦ cmpt 4673   × cxp 5072  dom cdm 5074  ran crn 5075   ↾ cres 5076   “ cima 5077   ∘ ccom 5078   Fn wfn 5842  ⟶wf 5843  –onto→wfo 5845  ‘cfv 5847  (class class class)co 6604  Fincfn 7899  Basecbs 15781  +gcplusg 15862  TopOpenctopn 16003  0gc0g 16021   Σg cgsu 16022  Mndcmnd 17215  Grpcgrp 17343  invgcminusg 17344  -gcsg 17345  CMndccmn 18114  Abelcabl 18115  TopOnctopon 20618  TopSpctps 20619  Homeochmeo 21466  TopGrpctgp 21785   tsums ctsu 21839 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-oi 8359  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-seq 12742  df-hash 13058  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-0g 16023  df-gsum 16024  df-topgen 16025  df-mre 16167  df-mrc 16168  df-acs 16170  df-plusf 17162  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-grp 17346  df-minusg 17347  df-sbg 17348  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-abl 18117  df-fbas 19662  df-fg 19663  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-ntr 20734  df-nei 20812  df-cn 20941  df-cnp 20942  df-tx 21275  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-tmd 21786  df-tgp 21787  df-tsms 21840 This theorem is referenced by:  tsmsxp  21868
 Copyright terms: Public domain W3C validator