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

Theorem tsmsxplem1 23504
Description: Lemma for tsmsxp 23506. (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))
21elin2d 4159 . . 3 (𝜑𝐾 ∈ Fin)
3 elfpw 9298 . . . . . . . 8 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾𝐴𝐾 ∈ Fin))
43simplbi 498 . . . . . . 7 (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾𝐴)
51, 4syl 17 . . . . . 6 (𝜑𝐾𝐴)
65sselda 3944 . . . . 5 ((𝜑𝑗𝐾) → 𝑗𝐴)
7 tsmsxp.b . . . . . 6 𝐵 = (Base‘𝐺)
8 tsmsxp.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
9 eqid 2736 . . . . . 6 (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
10 tsmsxp.g . . . . . . 7 (𝜑𝐺 ∈ CMnd)
1110adantr 481 . . . . . 6 ((𝜑𝑗𝐴) → 𝐺 ∈ CMnd)
12 tsmsxp.2 . . . . . . . 8 (𝜑𝐺 ∈ TopGrp)
13 tgptps 23431 . . . . . . . 8 (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
1412, 13syl 17 . . . . . . 7 (𝜑𝐺 ∈ TopSp)
1514adantr 481 . . . . . 6 ((𝜑𝑗𝐴) → 𝐺 ∈ TopSp)
16 tsmsxp.c . . . . . . 7 (𝜑𝐶𝑊)
1716adantr 481 . . . . . 6 ((𝜑𝑗𝐴) → 𝐶𝑊)
18 tsmsxp.f . . . . . . . . 9 (𝜑𝐹:(𝐴 × 𝐶)⟶𝐵)
19 fovcdm 7524 . . . . . . . . 9 ((𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
2018, 19syl3an1 1163 . . . . . . . 8 ((𝜑𝑗𝐴𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
21203expa 1118 . . . . . . 7 (((𝜑𝑗𝐴) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
2221fmpttd 7063 . . . . . 6 ((𝜑𝑗𝐴) → (𝑘𝐶 ↦ (𝑗𝐹𝑘)):𝐶𝐵)
23 tsmsxp.1 . . . . . 6 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
24 df-ima 5646 . . . . . . . 8 ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) = ran ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿)
258, 7tgptopon 23433 . . . . . . . . . . . . 13 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
2612, 25syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ (TopOn‘𝐵))
27 tsmsxp.l . . . . . . . . . . . 12 (𝜑𝐿𝐽)
28 toponss 22276 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿𝐽) → 𝐿𝐵)
2926, 27, 28syl2anc 584 . . . . . . . . . . 11 (𝜑𝐿𝐵)
3029adantr 481 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐿𝐵)
3130resmptd 5994 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿) = (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
3231rneqd 5893 . . . . . . . 8 ((𝜑𝑗𝐴) → ran ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ↾ 𝐿) = ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
3324, 32eqtrid 2788 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) = ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
34 tsmsxp.h . . . . . . . . . . . . 13 (𝜑𝐻:𝐴𝐵)
3534ffvelcdmda 7035 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ 𝐵)
36 tsmsxp.p . . . . . . . . . . . . 13 + = (+g𝐺)
37 eqid 2736 . . . . . . . . . . . . 13 (invg𝐺) = (invg𝐺)
38 tsmsxp.m . . . . . . . . . . . . 13 = (-g𝐺)
397, 36, 37, 38grpsubval 18796 . . . . . . . . . . . 12 (((𝐻𝑗) ∈ 𝐵𝑔𝐵) → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
4035, 39sylan 580 . . . . . . . . . . 11 (((𝜑𝑗𝐴) ∧ 𝑔𝐵) → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
4140mpteq2dva 5205 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) = (𝑔𝐵 ↦ ((𝐻𝑗) + ((invg𝐺)‘𝑔))))
42 tgpgrp 23429 . . . . . . . . . . . . . 14 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
4312, 42syl 17 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ Grp)
4443adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → 𝐺 ∈ Grp)
457, 37grpinvcl 18798 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑔𝐵) → ((invg𝐺)‘𝑔) ∈ 𝐵)
4644, 45sylan 580 . . . . . . . . . . 11 (((𝜑𝑗𝐴) ∧ 𝑔𝐵) → ((invg𝐺)‘𝑔) ∈ 𝐵)
477, 37grpinvf 18797 . . . . . . . . . . . . 13 (𝐺 ∈ Grp → (invg𝐺):𝐵𝐵)
4844, 47syl 17 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → (invg𝐺):𝐵𝐵)
4948feqmptd 6910 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → (invg𝐺) = (𝑔𝐵 ↦ ((invg𝐺)‘𝑔)))
50 eqidd 2737 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) = (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)))
51 oveq2 7365 . . . . . . . . . . 11 (𝑦 = ((invg𝐺)‘𝑔) → ((𝐻𝑗) + 𝑦) = ((𝐻𝑗) + ((invg𝐺)‘𝑔)))
5246, 49, 50, 51fmptco 7075 . . . . . . . . . 10 ((𝜑𝑗𝐴) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) = (𝑔𝐵 ↦ ((𝐻𝑗) + ((invg𝐺)‘𝑔))))
5341, 52eqtr4d 2779 . . . . . . . . 9 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) = ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)))
5412adantr 481 . . . . . . . . . . 11 ((𝜑𝑗𝐴) → 𝐺 ∈ TopGrp)
558, 37grpinvhmeo 23437 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → (invg𝐺) ∈ (𝐽Homeo𝐽))
5654, 55syl 17 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (invg𝐺) ∈ (𝐽Homeo𝐽))
57 eqid 2736 . . . . . . . . . . . 12 (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) = (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦))
5857, 7, 36, 8tgplacthmeo 23454 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ (𝐻𝑗) ∈ 𝐵) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
5954, 35, 58syl2anc 584 . . . . . . . . . 10 ((𝜑𝑗𝐴) → (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
60 hmeoco 23123 . . . . . . . . . 10 (((invg𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6156, 59, 60syl2anc 584 . . . . . . . . 9 ((𝜑𝑗𝐴) → ((𝑦𝐵 ↦ ((𝐻𝑗) + 𝑦)) ∘ (invg𝐺)) ∈ (𝐽Homeo𝐽))
6253, 61eqeltrd 2838 . . . . . . . 8 ((𝜑𝑗𝐴) → (𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ∈ (𝐽Homeo𝐽))
6327adantr 481 . . . . . . . 8 ((𝜑𝑗𝐴) → 𝐿𝐽)
64 hmeoima 23116 . . . . . . . 8 (((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿𝐽) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) ∈ 𝐽)
6562, 63, 64syl2anc 584 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝑔𝐵 ↦ ((𝐻𝑗) 𝑔)) “ 𝐿) ∈ 𝐽)
6633, 65eqeltrrd 2839 . . . . . 6 ((𝜑𝑗𝐴) → ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ∈ 𝐽)
67 tsmsxp.z . . . . . . . . 9 0 = (0g𝐺)
687, 67, 38grpsubid1 18832 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝐻𝑗) ∈ 𝐵) → ((𝐻𝑗) 0 ) = (𝐻𝑗))
6944, 35, 68syl2anc 584 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐻𝑗) 0 ) = (𝐻𝑗))
70 tsmsxp.3 . . . . . . . . 9 (𝜑0𝐿)
7170adantr 481 . . . . . . . 8 ((𝜑𝑗𝐴) → 0𝐿)
72 ovex 7390 . . . . . . . 8 ((𝐻𝑗) 0 ) ∈ V
73 eqid 2736 . . . . . . . . 9 (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) = (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))
74 oveq2 7365 . . . . . . . . 9 (𝑔 = 0 → ((𝐻𝑗) 𝑔) = ((𝐻𝑗) 0 ))
7573, 74elrnmpt1s 5912 . . . . . . . 8 (( 0𝐿 ∧ ((𝐻𝑗) 0 ) ∈ V) → ((𝐻𝑗) 0 ) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
7671, 72, 75sylancl 586 . . . . . . 7 ((𝜑𝑗𝐴) → ((𝐻𝑗) 0 ) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
7769, 76eqeltrrd 2839 . . . . . 6 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))
787, 8, 9, 11, 15, 17, 22, 23, 66, 77tsmsi 23485 . . . . 5 ((𝜑𝑗𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
796, 78syldan 591 . . . 4 ((𝜑𝑗𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
8079ralrimiva 3143 . . 3 (𝜑 → ∀𝑗𝐾𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
81 sseq1 3969 . . . . . 6 (𝑦 = (𝑓𝑗) → (𝑦𝑧 ↔ (𝑓𝑗) ⊆ 𝑧))
8281imbi1d 341 . . . . 5 (𝑦 = (𝑓𝑗) → ((𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ ((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
8382ralbidv 3174 . . . 4 (𝑦 = (𝑓𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
8483ac6sfi 9231 . . 3 ((𝐾 ∈ Fin ∧ ∀𝑗𝐾𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
852, 80, 84syl2anc 584 . 2 (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)))))
86 frn 6675 . . . . . . . . 9 (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
8786adantl 482 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
88 inss1 4188 . . . . . . . 8 (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
8987, 88sstrdi 3956 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
90 sspwuni 5060 . . . . . . 7 (ran 𝑓 ⊆ 𝒫 𝐶 ran 𝑓𝐶)
9189, 90sylib 217 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓𝐶)
92 tsmsxp.d . . . . . . . . 9 (𝜑𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93 elfpw 9298 . . . . . . . . . 10 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
9493simplbi 498 . . . . . . . . 9 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
95 rnss 5894 . . . . . . . . 9 (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
9692, 94, 953syl 18 . . . . . . . 8 (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
97 rnxpss 6124 . . . . . . . 8 ran (𝐴 × 𝐶) ⊆ 𝐶
9896, 97sstrdi 3956 . . . . . . 7 (𝜑 → ran 𝐷𝐶)
9998adantr 481 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷𝐶)
10091, 99unssd 4146 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
1012adantr 481 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
102 ffn 6668 . . . . . . . . . 10 (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
103102adantl 482 . . . . . . . . 9 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
104 dffn4 6762 . . . . . . . . 9 (𝑓 Fn 𝐾𝑓:𝐾onto→ran 𝑓)
105103, 104sylib 217 . . . . . . . 8 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾onto→ran 𝑓)
106 fofi 9282 . . . . . . . 8 ((𝐾 ∈ Fin ∧ 𝑓:𝐾onto→ran 𝑓) → ran 𝑓 ∈ Fin)
107101, 105, 106syl2anc 584 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
108 inss2 4189 . . . . . . . 8 (𝒫 𝐶 ∩ Fin) ⊆ Fin
10987, 108sstrdi 3956 . . . . . . 7 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
110 unifi 9285 . . . . . . 7 ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ran 𝑓 ∈ Fin)
111107, 109, 110syl2anc 584 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
112 elinel2 4156 . . . . . . . 8 (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
113 rnfi 9279 . . . . . . . 8 (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
11492, 112, 1133syl 18 . . . . . . 7 (𝜑 → ran 𝐷 ∈ Fin)
115114adantr 481 . . . . . 6 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
116 unfi 9116 . . . . . 6 (( ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
117111, 115, 116syl2anc 584 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
118 elfpw 9298 . . . . 5 (( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ (( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ ( ran 𝑓 ∪ ran 𝐷) ∈ Fin))
119100, 117, 118sylanbrc 583 . . . 4 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
120119adantrr 715 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
121 ssun2 4133 . . . 4 ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷)
122121a1i 11 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷))
123119adantlr 713 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
124 fvssunirn 6875 . . . . . . . . . . . . . 14 (𝑓𝑗) ⊆ ran 𝑓
125 ssun1 4132 . . . . . . . . . . . . . 14 ran 𝑓 ⊆ ( ran 𝑓 ∪ ran 𝐷)
126124, 125sstri 3953 . . . . . . . . . . . . 13 (𝑓𝑗) ⊆ ( ran 𝑓 ∪ ran 𝐷)
127 id 22 . . . . . . . . . . . . 13 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → 𝑧 = ( ran 𝑓 ∪ ran 𝐷))
128126, 127sseqtrrid 3997 . . . . . . . . . . . 12 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (𝑓𝑗) ⊆ 𝑧)
129 pm5.5 361 . . . . . . . . . . . 12 ((𝑓𝑗) ⊆ 𝑧 → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
130128, 129syl 17 . . . . . . . . . . 11 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
131 reseq2 5932 . . . . . . . . . . . . 13 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷)))
132131oveq2d 7373 . . . . . . . . . . . 12 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))))
133132eleq1d 2822 . . . . . . . . . . 11 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
134130, 133bitrd 278 . . . . . . . . . 10 (𝑧 = ( ran 𝑓 ∪ ran 𝐷) → (((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) ↔ (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
135134rspcv 3577 . . . . . . . . 9 (( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
136123, 135syl 17 . . . . . . . 8 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
13710ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
138 cmnmnd 19579 . . . . . . . . . . . . 13 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
139137, 138syl 17 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
140 simplr 767 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗𝐾)
141117adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ∈ Fin)
142100adantlr 713 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
143142sselda 3944 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → 𝑘𝐶)
14418adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
145144, 6jca 512 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴))
146193expa 1118 . . . . . . . . . . . . . . . . 17 (((𝐹:(𝐴 × 𝐶)⟶𝐵𝑗𝐴) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
147145, 146sylan 580 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐾) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
148147adantlr 713 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149143, 148syldan 591 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
150149fmpttd 7063 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):( ran 𝑓 ∪ ran 𝐷)⟶𝐵)
151 eqid 2736 . . . . . . . . . . . . . 14 (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
152 ovexd 7392 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
15367fvexi 6856 . . . . . . . . . . . . . . 15 0 ∈ V
154153a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
155151, 141, 152, 154fsuppmptdm 9316 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
1567, 67, 137, 141, 150, 155gsumcl 19692 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
157 velsn 4602 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
158 ovres 7520 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
159157, 158sylanbr 582 . . . . . . . . . . . . . . . 16 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
160 oveq1 7364 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
161160adantr 481 . . . . . . . . . . . . . . . 16 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
162159, 161eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑗𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
163162mpteq2dva 5205 . . . . . . . . . . . . . 14 (𝑦 = 𝑗 → (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
164163oveq2d 7373 . . . . . . . . . . . . 13 (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
1657, 164gsumsn 19731 . . . . . . . . . . . 12 ((𝐺 ∈ Mnd ∧ 𝑗𝐾 ∧ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
166139, 140, 156, 165syl3anc 1371 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
167 snfi 8988 . . . . . . . . . . . . 13 {𝑗} ∈ Fin
168167a1i 11 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
16918ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
1706adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗𝐴)
171170snssd 4769 . . . . . . . . . . . . . 14 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
172 xpss12 5648 . . . . . . . . . . . . . 14 (({𝑗} ⊆ 𝐴 ∧ ( ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
173171, 142, 172syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
174169, 173fssresd 6709 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))):({𝑗} × ( ran 𝑓 ∪ ran 𝐷))⟶𝐵)
175 xpfi 9261 . . . . . . . . . . . . . 14 (({𝑗} ∈ Fin ∧ ( ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
176167, 141, 175sylancr 587 . . . . . . . . . . . . 13 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
177174, 176, 154fdmfifsupp 9315 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
1787, 67, 137, 168, 141, 174, 177gsumxp 19753 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))𝑘))))))
179142resmptd 5994 . . . . . . . . . . . 12 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
180179oveq2d 7373 . . . . . . . . . . 11 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ ( ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
181166, 178, 1803eqtr4rd 2787 . . . . . . . . . 10 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))))
182181eleq1d 2822 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))
183 ovex 7390 . . . . . . . . . . 11 ((𝐻𝑗) 𝑔) ∈ V
18473, 183elrnmpti 5915 . . . . . . . . . 10 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) ↔ ∃𝑔𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔))
185 isabl 19566 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
18643, 10, 185sylanbrc 583 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ Abel)
187186ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝐺 ∈ Abel)
1886, 35syldan 591 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝐾) → (𝐻𝑗) ∈ 𝐵)
189188ad2antrr 724 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → (𝐻𝑗) ∈ 𝐵)
19029ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿𝐵)
191190sselda 3944 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝑔𝐵)
1927, 38, 187, 189, 191ablnncan 19599 . . . . . . . . . . . . 13 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐻𝑗) ((𝐻𝑗) 𝑔)) = 𝑔)
193 simpr 485 . . . . . . . . . . . . 13 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → 𝑔𝐿)
194192, 193eqeltrd 2838 . . . . . . . . . . . 12 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐻𝑗) ((𝐻𝑗) 𝑔)) ∈ 𝐿)
195 oveq2 7365 . . . . . . . . . . . . 13 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) = ((𝐻𝑗) ((𝐻𝑗) 𝑔)))
196195eleq1d 2822 . . . . . . . . . . . 12 ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → (((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻𝑗) ((𝐻𝑗) 𝑔)) ∈ 𝐿))
197194, 196syl5ibrcom 246 . . . . . . . . . . 11 ((((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
198197rexlimdva 3152 . . . . . . . . . 10 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = ((𝐻𝑗) 𝑔) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
199184, 198biimtrid 241 . . . . . . . . 9 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
200182, 199sylbid 239 . . . . . . . 8 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ ( ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔)) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
201136, 200syld 47 . . . . . . 7 (((𝜑𝑗𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
202201an32s 650 . . . . . 6 (((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203202ralimdva 3164 . . . . 5 ((𝜑𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))) → ∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204203impr 455 . . . 4 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
205 fveq2 6842 . . . . . . 7 (𝑗 = 𝑥 → (𝐻𝑗) = (𝐻𝑥))
206 sneq 4596 . . . . . . . . . 10 (𝑗 = 𝑥 → {𝑗} = {𝑥})
207206xpeq1d 5662 . . . . . . . . 9 (𝑗 = 𝑥 → ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))
208207reseq2d 5937 . . . . . . . 8 (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))
209208oveq2d 7373 . . . . . . 7 (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))))
210205, 209oveq12d 7375 . . . . . 6 (𝑗 = 𝑥 → ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) = ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))))
211210eleq1d 2822 . . . . 5 (𝑗 = 𝑥 → (((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
212211cbvralvw 3225 . . . 4 (∀𝑗𝐾 ((𝐻𝑗) (𝐺 Σg (𝐹 ↾ ({𝑗} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
213204, 212sylib 217 . . 3 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
214 sseq2 3970 . . . . 5 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (ran 𝐷𝑛 ↔ ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷)))
215 xpeq2 5654 . . . . . . . . . 10 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))
216215reseq2d 5937 . . . . . . . . 9 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))
217216oveq2d 7373 . . . . . . . 8 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷)))))
218217oveq2d 7373 . . . . . . 7 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))))
219218eleq1d 2822 . . . . . 6 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
220219ralbidv 3174 . . . . 5 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → (∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
221214, 220anbi12d 631 . . . 4 (𝑛 = ( ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)))
222221rspcev 3581 . . 3 ((( ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ ( ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × ( ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
223120, 122, 213, 222syl12anc 835 . 2 ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗𝐾𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔𝐿 ↦ ((𝐻𝑗) 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
22485, 223exlimddv 1938 1 (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷𝑛 ∧ ∀𝑥𝐾 ((𝐻𝑥) (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  cun 3908  cin 3909  wss 3910  𝒫 cpw 4560  {csn 4586   cuni 4865  cmpt 5188   × cxp 5631  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  ccom 5637   Fn wfn 6491  wf 6492  ontowfo 6494  cfv 6496  (class class class)co 7357  Fincfn 8883  Basecbs 17083  +gcplusg 17133  TopOpenctopn 17303  0gc0g 17321   Σg cgsu 17322  Mndcmnd 18556  Grpcgrp 18748  invgcminusg 18749  -gcsg 18750  CMndccmn 19562  Abelcabl 19563  TopOnctopon 22259  TopSpctps 22281  Homeochmeo 23104  TopGrpctgp 23422   tsums ctsu 23477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-0g 17323  df-gsum 17324  df-topgen 17325  df-mre 17466  df-mrc 17467  df-acs 17469  df-plusf 18496  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-abl 19565  df-fbas 20793  df-fg 20794  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-ntr 22371  df-nei 22449  df-cn 22578  df-cnp 22579  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-tmd 23423  df-tgp 23424  df-tsms 23478
This theorem is referenced by:  tsmsxp  23506
  Copyright terms: Public domain W3C validator