| Step | Hyp | Ref
| Expression |
| 1 | | tsmsxp.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin)) |
| 2 | 1 | elin2d 4205 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Fin) |
| 3 | | elfpw 9394 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin)) |
| 4 | 3 | simplbi 497 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴) |
| 5 | 1, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ⊆ 𝐴) |
| 6 | 5 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝑗 ∈ 𝐴) |
| 7 | | tsmsxp.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 8 | | tsmsxp.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
| 9 | | eqid 2737 |
. . . . . 6
⊢
(𝒫 𝐶 ∩
Fin) = (𝒫 𝐶 ∩
Fin) |
| 10 | | tsmsxp.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ CMnd) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ CMnd) |
| 12 | | tsmsxp.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
| 13 | | tgptps 24088 |
. . . . . . . 8
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) |
| 14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TopSp) |
| 15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopSp) |
| 16 | | tsmsxp.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑊) |
| 17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
| 18 | | tsmsxp.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
| 19 | | fovcdm 7603 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
| 20 | 18, 19 | syl3an1 1164 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
| 21 | 20 | 3expa 1119 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
| 22 | 21 | fmpttd 7135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)):𝐶⟶𝐵) |
| 23 | | tsmsxp.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)))) |
| 24 | | df-ima 5698 |
. . . . . . . 8
⊢ ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) |
| 25 | 8, 7 | tgptopon 24090 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵)) |
| 26 | 12, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵)) |
| 27 | | tsmsxp.l |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ 𝐽) |
| 28 | | toponss 22933 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿 ∈ 𝐽) → 𝐿 ⊆ 𝐵) |
| 29 | 26, 27, 28 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ⊆ 𝐵) |
| 30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ⊆ 𝐵) |
| 31 | 30 | resmptd 6058 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
| 32 | 31 | rneqd 5949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
| 33 | 24, 32 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
| 34 | | tsmsxp.h |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
| 35 | 34 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ 𝐵) |
| 36 | | tsmsxp.p |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝐺) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 38 | | tsmsxp.m |
. . . . . . . . . . . . 13
⊢ − =
(-g‘𝐺) |
| 39 | 7, 36, 37, 38 | grpsubval 19003 |
. . . . . . . . . . . 12
⊢ (((𝐻‘𝑗) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔))) |
| 40 | 35, 39 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔))) |
| 41 | 40 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔)))) |
| 42 | | tgpgrp 24086 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
| 43 | 12, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ Grp) |
| 45 | 7, 37 | grpinvcl 19005 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵) |
| 46 | 44, 45 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵) |
| 47 | 7, 37 | grpinvf 19004 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):𝐵⟶𝐵) |
| 48 | 44, 47 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺):𝐵⟶𝐵) |
| 49 | 48 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) = (𝑔 ∈ 𝐵 ↦ ((invg‘𝐺)‘𝑔))) |
| 50 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦))) |
| 51 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = ((invg‘𝐺)‘𝑔) → ((𝐻‘𝑗) + 𝑦) = ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔))) |
| 52 | 46, 49, 50, 51 | fmptco 7149 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔)))) |
| 53 | 41, 52 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺))) |
| 54 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopGrp) |
| 55 | 8, 37 | grpinvhmeo 24094 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ (𝐽Homeo𝐽)) |
| 56 | 54, 55 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) ∈ (𝐽Homeo𝐽)) |
| 57 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) |
| 58 | 57, 7, 36, 8 | tgplacthmeo 24111 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ (𝐻‘𝑗) ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) |
| 59 | 54, 35, 58 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) |
| 60 | | hmeoco 23780 |
. . . . . . . . . 10
⊢
(((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
| 61 | 56, 59, 60 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
| 62 | 53, 61 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽)) |
| 63 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ∈ 𝐽) |
| 64 | | hmeoima 23773 |
. . . . . . . 8
⊢ (((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿 ∈ 𝐽) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽) |
| 65 | 62, 63, 64 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽) |
| 66 | 33, 65 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ 𝐽) |
| 67 | | tsmsxp.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
| 68 | 7, 67, 38 | grpsubid1 19043 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝐻‘𝑗) ∈ 𝐵) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗)) |
| 69 | 44, 35, 68 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗)) |
| 70 | | tsmsxp.3 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝐿) |
| 71 | 70 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ 𝐿) |
| 72 | | ovex 7464 |
. . . . . . . 8
⊢ ((𝐻‘𝑗) − 0 ) ∈
V |
| 73 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) |
| 74 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑔 = 0 → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) − 0 )) |
| 75 | 73, 74 | elrnmpt1s 5970 |
. . . . . . . 8
⊢ (( 0 ∈ 𝐿 ∧ ((𝐻‘𝑗) − 0 ) ∈ V) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
| 76 | 71, 72, 75 | sylancl 586 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
| 77 | 69, 76 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
| 78 | 7, 8, 9, 11, 15, 17, 22, 23, 66, 77 | tsmsi 24142 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 79 | 6, 78 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 80 | 79 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 81 | | sseq1 4009 |
. . . . . 6
⊢ (𝑦 = (𝑓‘𝑗) → (𝑦 ⊆ 𝑧 ↔ (𝑓‘𝑗) ⊆ 𝑧)) |
| 82 | 81 | imbi1d 341 |
. . . . 5
⊢ (𝑦 = (𝑓‘𝑗) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
| 83 | 82 | ralbidv 3178 |
. . . 4
⊢ (𝑦 = (𝑓‘𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
| 84 | 83 | ac6sfi 9320 |
. . 3
⊢ ((𝐾 ∈ Fin ∧ ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
| 85 | 2, 80, 84 | syl2anc 584 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
| 86 | | frn 6743 |
. . . . . . . . 9
⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin)) |
| 87 | 86 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin)) |
| 88 | | inss1 4237 |
. . . . . . . 8
⊢
(𝒫 𝐶 ∩
Fin) ⊆ 𝒫 𝐶 |
| 89 | 87, 88 | sstrdi 3996 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶) |
| 90 | | sspwuni 5100 |
. . . . . . 7
⊢ (ran
𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶) |
| 91 | 89, 90 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ⊆ 𝐶) |
| 92 | | tsmsxp.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)) |
| 93 | | elfpw 9394 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin)) |
| 94 | 93 | simplbi 497 |
. . . . . . . . 9
⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶)) |
| 95 | | rnss 5950 |
. . . . . . . . 9
⊢ (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶)) |
| 96 | 92, 94, 95 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶)) |
| 97 | | rnxpss 6192 |
. . . . . . . 8
⊢ ran
(𝐴 × 𝐶) ⊆ 𝐶 |
| 98 | 96, 97 | sstrdi 3996 |
. . . . . . 7
⊢ (𝜑 → ran 𝐷 ⊆ 𝐶) |
| 99 | 98 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ⊆ 𝐶) |
| 100 | 91, 99 | unssd 4192 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) |
| 101 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin) |
| 102 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾) |
| 103 | 102 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾) |
| 104 | | dffn4 6826 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝐾 ↔ 𝑓:𝐾–onto→ran 𝑓) |
| 105 | 103, 104 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾–onto→ran 𝑓) |
| 106 | | fofi 9351 |
. . . . . . . 8
⊢ ((𝐾 ∈ Fin ∧ 𝑓:𝐾–onto→ran 𝑓) → ran 𝑓 ∈ Fin) |
| 107 | 101, 105,
106 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin) |
| 108 | | inss2 4238 |
. . . . . . . 8
⊢
(𝒫 𝐶 ∩
Fin) ⊆ Fin |
| 109 | 87, 108 | sstrdi 3996 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin) |
| 110 | | unifi 9384 |
. . . . . . 7
⊢ ((ran
𝑓 ∈ Fin ∧ ran
𝑓 ⊆ Fin) → ∪ ran 𝑓 ∈ Fin) |
| 111 | 107, 109,
110 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ∈ Fin) |
| 112 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin) |
| 113 | | rnfi 9380 |
. . . . . . . 8
⊢ (𝐷 ∈ Fin → ran 𝐷 ∈ Fin) |
| 114 | 92, 112, 113 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝐷 ∈ Fin) |
| 115 | 114 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin) |
| 116 | | unfi 9211 |
. . . . . 6
⊢ ((∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) |
| 117 | 111, 115,
116 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) |
| 118 | | elfpw 9394 |
. . . . 5
⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ (∪ ran
𝑓 ∪ ran 𝐷) ∈ Fin)) |
| 119 | 100, 117,
118 | sylanbrc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin)) |
| 120 | 119 | adantrr 717 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → (∪
ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin)) |
| 121 | | ssun2 4179 |
. . . 4
⊢ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) |
| 122 | 121 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷)) |
| 123 | 119 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin)) |
| 124 | | fvssunirn 6939 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘𝑗) ⊆ ∪ ran
𝑓 |
| 125 | | ssun1 4178 |
. . . . . . . . . . . . . 14
⊢ ∪ ran 𝑓 ⊆ (∪ ran
𝑓 ∪ ran 𝐷) |
| 126 | 124, 125 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ (𝑓‘𝑗) ⊆ (∪ ran
𝑓 ∪ ran 𝐷) |
| 127 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → 𝑧 = (∪ ran 𝑓 ∪ ran 𝐷)) |
| 128 | 126, 127 | sseqtrrid 4027 |
. . . . . . . . . . . 12
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝑓‘𝑗) ⊆ 𝑧) |
| 129 | | pm5.5 361 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑗) ⊆ 𝑧 → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 130 | 128, 129 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 131 | | reseq2 5992 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) |
| 132 | 131 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷)))) |
| 133 | 132 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 134 | 130, 133 | bitrd 279 |
. . . . . . . . . 10
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 135 | 134 | rspcv 3618 |
. . . . . . . . 9
⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 136 | 123, 135 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 137 | 10 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd) |
| 138 | | cmnmnd 19815 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
| 139 | 137, 138 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd) |
| 140 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐾) |
| 141 | 117 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) |
| 142 | 100 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) |
| 143 | 142 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → 𝑘 ∈ 𝐶) |
| 144 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
| 145 | 144, 6 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴)) |
| 146 | 19 | 3expa 1119 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
| 147 | 145, 146 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
| 148 | 147 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
| 149 | 143, 148 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵) |
| 150 | 149 | fmpttd 7135 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):(∪ ran 𝑓 ∪ ran 𝐷)⟶𝐵) |
| 151 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) |
| 152 | | ovexd 7466 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V) |
| 153 | 67 | fvexi 6920 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
| 154 | 153 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V) |
| 155 | 151, 141,
152, 154 | fsuppmptdm 9416 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 ) |
| 156 | 7, 67, 137, 141, 150, 155 | gsumcl 19933 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
| 157 | | velsn 4642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗) |
| 158 | | ovres 7599 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘)) |
| 159 | 157, 158 | sylanbr 582 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘)) |
| 160 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘)) |
| 161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘)) |
| 162 | 159, 161 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘)) |
| 163 | 162 | mpteq2dva 5242 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑗 → (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) |
| 164 | 163 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
| 165 | 7, 164 | gsumsn 19972 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
| 166 | 139, 140,
156, 165 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
| 167 | | snfi 9083 |
. . . . . . . . . . . . 13
⊢ {𝑗} ∈ Fin |
| 168 | 167 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin) |
| 169 | 18 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
| 170 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐴) |
| 171 | 170 | snssd 4809 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴) |
| 172 | | xpss12 5700 |
. . . . . . . . . . . . . 14
⊢ (({𝑗} ⊆ 𝐴 ∧ (∪ ran
𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶)) |
| 173 | 171, 142,
172 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶)) |
| 174 | 169, 173 | fssresd 6775 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))):({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))⟶𝐵) |
| 175 | | xpfi 9358 |
. . . . . . . . . . . . . 14
⊢ (({𝑗} ∈ Fin ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ∈ Fin) |
| 176 | 167, 141,
175 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ∈ Fin) |
| 177 | 174, 176,
154 | fdmfifsupp 9415 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))) finSupp 0 ) |
| 178 | 7, 67, 137, 168, 141, 174, 177 | gsumxp 19994 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘)))))) |
| 179 | 142 | resmptd 6058 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷)) = (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) |
| 180 | 179 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
| 181 | 166, 178,
180 | 3eqtr4rd 2788 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) |
| 182 | 181 | eleq1d 2826 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
| 183 | | ovex 7464 |
. . . . . . . . . . 11
⊢ ((𝐻‘𝑗) − 𝑔) ∈ V |
| 184 | 73, 183 | elrnmpti 5973 |
. . . . . . . . . 10
⊢ ((𝐺 Σg
(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ ∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔)) |
| 185 | | isabl 19802 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
| 186 | 43, 10, 185 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Abel) |
| 187 | 186 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝐺 ∈ Abel) |
| 188 | 6, 35 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐻‘𝑗) ∈ 𝐵) |
| 189 | 188 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → (𝐻‘𝑗) ∈ 𝐵) |
| 190 | 29 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿 ⊆ 𝐵) |
| 191 | 190 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐵) |
| 192 | 7, 38, 187, 189, 191 | ablnncan 19838 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) = 𝑔) |
| 193 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐿) |
| 194 | 192, 193 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿) |
| 195 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ ((𝐺 Σg
(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔))) |
| 196 | 195 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ ((𝐺 Σg
(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿)) |
| 197 | 194, 196 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 198 | 197 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 199 | 184, 198 | biimtrid 242 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 200 | 182, 199 | sylbid 240 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 201 | 136, 200 | syld 47 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 202 | 201 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗 ∈ 𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 203 | 202 | ralimdva 3167 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 204 | 203 | impr 454 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿) |
| 205 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑗 = 𝑥 → (𝐻‘𝑗) = (𝐻‘𝑥)) |
| 206 | | sneq 4636 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥}) |
| 207 | 206 | xpeq1d 5714 |
. . . . . . . . 9
⊢ (𝑗 = 𝑥 → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) = ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))) |
| 208 | 207 | reseq2d 5997 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))) |
| 209 | 208 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) |
| 210 | 205, 209 | oveq12d 7449 |
. . . . . 6
⊢ (𝑗 = 𝑥 → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))))) |
| 211 | 210 | eleq1d 2826 |
. . . . 5
⊢ (𝑗 = 𝑥 → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 212 | 211 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑗 ∈
𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿) |
| 213 | 204, 212 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿) |
| 214 | | sseq2 4010 |
. . . . 5
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷))) |
| 215 | | xpeq2 5706 |
. . . . . . . . . 10
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))) |
| 216 | 215 | reseq2d 5997 |
. . . . . . . . 9
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))) |
| 217 | 216 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) |
| 218 | 217 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))))) |
| 219 | 218 | eleq1d 2826 |
. . . . . 6
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 220 | 219 | ralbidv 3178 |
. . . . 5
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
| 221 | 214, 220 | anbi12d 632 |
. . . 4
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿))) |
| 222 | 221 | rspcev 3622 |
. . 3
⊢ (((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿)) |
| 223 | 120, 122,
213, 222 | syl12anc 837 |
. 2
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿)) |
| 224 | 85, 223 | exlimddv 1935 |
1
⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿)) |