Step | Hyp | Ref
| Expression |
1 | | tsmsxp.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin)) |
2 | | elfpw 8151 |
. . . . 5
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin)) |
3 | 2 | simprbi 479 |
. . . 4
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ∈ Fin) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Fin) |
5 | 2 | simplbi 475 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴) |
6 | 1, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ⊆ 𝐴) |
7 | 6 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝑗 ∈ 𝐴) |
8 | | tsmsxp.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
9 | | tsmsxp.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
10 | | eqid 2610 |
. . . . . 6
⊢
(𝒫 𝐶 ∩
Fin) = (𝒫 𝐶 ∩
Fin) |
11 | | tsmsxp.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ CMnd) |
12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ CMnd) |
13 | | tsmsxp.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
14 | | tgptps 21694 |
. . . . . . . 8
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TopSp) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopSp) |
17 | | tsmsxp.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑊) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
19 | | tsmsxp.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
20 | | fovrn 6702 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
21 | 19, 20 | syl3an1 1351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
22 | 21 | 3expa 1257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
23 | | eqid 2610 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) |
24 | 22, 23 | fmptd 6292 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)):𝐶⟶𝐵) |
25 | | tsmsxp.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)))) |
26 | | df-ima 5051 |
. . . . . . . 8
⊢ ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) |
27 | 9, 8 | tgptopon 21696 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵)) |
28 | 13, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵)) |
29 | | tsmsxp.l |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ 𝐽) |
30 | | toponss 20544 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿 ∈ 𝐽) → 𝐿 ⊆ 𝐵) |
31 | 28, 29, 30 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ⊆ 𝐵) |
32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ⊆ 𝐵) |
33 | 32 | resmptd 5371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
34 | 33 | rneqd 5274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
35 | 26, 34 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
36 | | tsmsxp.h |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
37 | 36 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ 𝐵) |
38 | | tsmsxp.p |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝐺) |
39 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(invg‘𝐺) = (invg‘𝐺) |
40 | | tsmsxp.m |
. . . . . . . . . . . . 13
⊢ − =
(-g‘𝐺) |
41 | 8, 38, 39, 40 | grpsubval 17288 |
. . . . . . . . . . . 12
⊢ (((𝐻‘𝑗) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔))) |
42 | 37, 41 | sylan 487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔))) |
43 | 42 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔)))) |
44 | | tgpgrp 21692 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
45 | 13, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ Grp) |
46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ Grp) |
47 | 8, 39 | grpinvcl 17290 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵) |
48 | 46, 47 | sylan 487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵) |
49 | 8, 39 | grpinvf 17289 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):𝐵⟶𝐵) |
50 | 46, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺):𝐵⟶𝐵) |
51 | 50 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) = (𝑔 ∈ 𝐵 ↦ ((invg‘𝐺)‘𝑔))) |
52 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦))) |
53 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑦 = ((invg‘𝐺)‘𝑔) → ((𝐻‘𝑗) + 𝑦) = ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔))) |
54 | 48, 51, 52, 53 | fmptco 6303 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) +
((invg‘𝐺)‘𝑔)))) |
55 | 43, 54 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺))) |
56 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopGrp) |
57 | 9, 39 | grpinvhmeo 21700 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ (𝐽Homeo𝐽)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) ∈ (𝐽Homeo𝐽)) |
59 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) |
60 | 59, 8, 38, 9 | tgplacthmeo 21717 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ (𝐻‘𝑗) ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) |
61 | 56, 37, 60 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) |
62 | | hmeoco 21385 |
. . . . . . . . . 10
⊢
(((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
63 | 58, 61, 62 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽)) |
64 | 55, 63 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽)) |
65 | 29 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ∈ 𝐽) |
66 | | hmeoima 21378 |
. . . . . . . 8
⊢ (((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿 ∈ 𝐽) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽) |
67 | 64, 65, 66 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽) |
68 | 35, 67 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ 𝐽) |
69 | | tsmsxp.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
70 | 8, 69, 40 | grpsubid1 17323 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝐻‘𝑗) ∈ 𝐵) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗)) |
71 | 46, 37, 70 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗)) |
72 | | tsmsxp.3 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝐿) |
73 | 72 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ 𝐿) |
74 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝐻‘𝑗) − 0 ) ∈
V |
75 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) |
76 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑔 = 0 → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) − 0 )) |
77 | 75, 76 | elrnmpt1s 5294 |
. . . . . . . 8
⊢ (( 0 ∈ 𝐿 ∧ ((𝐻‘𝑗) − 0 ) ∈ V) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
78 | 73, 74, 77 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
79 | 71, 78 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) |
80 | 8, 9, 10, 12, 16, 18, 24, 25, 68, 79 | tsmsi 21747 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
81 | 7, 80 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
82 | 81 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
83 | | sseq1 3589 |
. . . . . 6
⊢ (𝑦 = (𝑓‘𝑗) → (𝑦 ⊆ 𝑧 ↔ (𝑓‘𝑗) ⊆ 𝑧)) |
84 | 83 | imbi1d 330 |
. . . . 5
⊢ (𝑦 = (𝑓‘𝑗) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
85 | 84 | ralbidv 2969 |
. . . 4
⊢ (𝑦 = (𝑓‘𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
86 | 85 | ac6sfi 8089 |
. . 3
⊢ ((𝐾 ∈ Fin ∧ ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
87 | 4, 82, 86 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) |
88 | | frn 5966 |
. . . . . . . . 9
⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin)) |
89 | 88 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin)) |
90 | | inss1 3795 |
. . . . . . . 8
⊢
(𝒫 𝐶 ∩
Fin) ⊆ 𝒫 𝐶 |
91 | 89, 90 | syl6ss 3580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶) |
92 | | sspwuni 4547 |
. . . . . . 7
⊢ (ran
𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶) |
93 | 91, 92 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ⊆ 𝐶) |
94 | | tsmsxp.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)) |
95 | | elfpw 8151 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin)) |
96 | 95 | simplbi 475 |
. . . . . . . . 9
⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶)) |
97 | | rnss 5275 |
. . . . . . . . 9
⊢ (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶)) |
98 | 94, 96, 97 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶)) |
99 | | rnxpss 5485 |
. . . . . . . 8
⊢ ran
(𝐴 × 𝐶) ⊆ 𝐶 |
100 | 98, 99 | syl6ss 3580 |
. . . . . . 7
⊢ (𝜑 → ran 𝐷 ⊆ 𝐶) |
101 | 100 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ⊆ 𝐶) |
102 | 93, 101 | unssd 3751 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) |
103 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin) |
104 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾) |
105 | 104 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾) |
106 | | dffn4 6034 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝐾 ↔ 𝑓:𝐾–onto→ran 𝑓) |
107 | 105, 106 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾–onto→ran 𝑓) |
108 | | fofi 8135 |
. . . . . . . 8
⊢ ((𝐾 ∈ Fin ∧ 𝑓:𝐾–onto→ran 𝑓) → ran 𝑓 ∈ Fin) |
109 | 103, 107,
108 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin) |
110 | | inss2 3796 |
. . . . . . . 8
⊢
(𝒫 𝐶 ∩
Fin) ⊆ Fin |
111 | 89, 110 | syl6ss 3580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin) |
112 | | unifi 8138 |
. . . . . . 7
⊢ ((ran
𝑓 ∈ Fin ∧ ran
𝑓 ⊆ Fin) → ∪ ran 𝑓 ∈ Fin) |
113 | 109, 111,
112 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ∈ Fin) |
114 | 95 | simprbi 479 |
. . . . . . . 8
⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin) |
115 | | rnfi 8132 |
. . . . . . . 8
⊢ (𝐷 ∈ Fin → ran 𝐷 ∈ Fin) |
116 | 94, 114, 115 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝐷 ∈ Fin) |
117 | 116 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin) |
118 | | unfi 8112 |
. . . . . 6
⊢ ((∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) |
119 | 113, 117,
118 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) |
120 | | elfpw 8151 |
. . . . 5
⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ (∪ ran
𝑓 ∪ ran 𝐷) ∈ Fin)) |
121 | 102, 119,
120 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin)) |
122 | 121 | adantrr 749 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → (∪
ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin)) |
123 | | ssun2 3739 |
. . . 4
⊢ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) |
124 | 123 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷)) |
125 | 121 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin)) |
126 | | fvssunirn 6127 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘𝑗) ⊆ ∪ ran
𝑓 |
127 | | ssun1 3738 |
. . . . . . . . . . . . . 14
⊢ ∪ ran 𝑓 ⊆ (∪ ran
𝑓 ∪ ran 𝐷) |
128 | 126, 127 | sstri 3577 |
. . . . . . . . . . . . 13
⊢ (𝑓‘𝑗) ⊆ (∪ ran
𝑓 ∪ ran 𝐷) |
129 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → 𝑧 = (∪ ran 𝑓 ∪ ran 𝐷)) |
130 | 128, 129 | syl5sseqr 3617 |
. . . . . . . . . . . 12
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝑓‘𝑗) ⊆ 𝑧) |
131 | | pm5.5 350 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑗) ⊆ 𝑧 → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
133 | | reseq2 5312 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) |
134 | 133 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷)))) |
135 | 134 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
136 | 132, 135 | bitrd 267 |
. . . . . . . . . 10
⊢ (𝑧 = (∪
ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
137 | 136 | rspcv 3278 |
. . . . . . . . 9
⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
138 | 125, 137 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
139 | 11 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd) |
140 | | cmnmnd 18031 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd) |
142 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐾) |
143 | 119 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) |
144 | 102 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) |
145 | 144 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → 𝑘 ∈ 𝐶) |
146 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
147 | 146, 7 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴)) |
148 | 20 | 3expa 1257 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
149 | 147, 148 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
150 | 149 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵) |
151 | 145, 150 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵) |
152 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) |
153 | 151, 152 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):(∪ ran 𝑓 ∪ ran 𝐷)⟶𝐵) |
154 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑗𝐹𝑘) ∈ V |
155 | 154 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V) |
156 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐺) ∈ V |
157 | 69, 156 | eqeltri 2684 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
158 | 157 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V) |
159 | 152, 143,
155, 158 | fsuppmptdm 8169 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 ) |
160 | 8, 69, 139, 143, 153, 159 | gsumcl 18139 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) |
161 | | velsn 4141 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗) |
162 | | ovres 6698 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘)) |
163 | 161, 162 | sylanbr 489 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘)) |
164 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘)) |
165 | 164 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘)) |
166 | 163, 165 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘)) |
167 | 166 | mpteq2dva 4672 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑗 → (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) |
168 | 167 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
169 | 8, 168 | gsumsn 18177 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
170 | 141, 142,
160, 169 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
171 | | snfi 7923 |
. . . . . . . . . . . . 13
⊢ {𝑗} ∈ Fin |
172 | 171 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin) |
173 | 19 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
174 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐴) |
175 | 174 | snssd 4281 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴) |
176 | | xpss12 5148 |
. . . . . . . . . . . . . 14
⊢ (({𝑗} ⊆ 𝐴 ∧ (∪ ran
𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶)) |
177 | 175, 144,
176 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶)) |
178 | 173, 177 | fssresd 5984 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))):({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))⟶𝐵) |
179 | | xpfi 8116 |
. . . . . . . . . . . . . 14
⊢ (({𝑗} ∈ Fin ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ∈ Fin) |
180 | 171, 143,
179 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) ∈ Fin) |
181 | 178, 180,
158 | fdmfifsupp 8168 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))) finSupp 0 ) |
182 | 8, 69, 139, 172, 143, 178, 181 | gsumxp 18198 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))𝑘)))))) |
183 | 144 | resmptd 5371 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷)) = (𝑘 ∈ (∪ ran
𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) |
184 | 183 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))) |
185 | 170, 182,
184 | 3eqtr4rd 2655 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) |
186 | 185 | eleq1d 2672 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) |
187 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐻‘𝑗) − 𝑔) ∈ V |
188 | 75, 187 | elrnmpti 5297 |
. . . . . . . . . 10
⊢ ((𝐺 Σg
(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ ∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔)) |
189 | | isabl 18020 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
190 | 45, 11, 189 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Abel) |
191 | 190 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝐺 ∈ Abel) |
192 | 7, 37 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐻‘𝑗) ∈ 𝐵) |
193 | 192 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → (𝐻‘𝑗) ∈ 𝐵) |
194 | 31 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿 ⊆ 𝐵) |
195 | 194 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐵) |
196 | 8, 40, 191, 193, 195 | ablnncan 18049 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) = 𝑔) |
197 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐿) |
198 | 196, 197 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿) |
199 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ ((𝐺 Σg
(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔))) |
200 | 199 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝐺 Σg
(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿)) |
201 | 198, 200 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
202 | 201 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
203 | 188, 202 | syl5bi 231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
204 | 186, 203 | sylbid 229 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran
𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
205 | 138, 204 | syld 46 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
206 | 205 | an32s 842 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗 ∈ 𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
207 | 206 | ralimdva 2945 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
208 | 207 | impr 647 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿) |
209 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = 𝑥 → (𝐻‘𝑗) = (𝐻‘𝑥)) |
210 | | sneq 4135 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥}) |
211 | 210 | xpeq1d 5062 |
. . . . . . . . 9
⊢ (𝑗 = 𝑥 → ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)) = ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))) |
212 | 211 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))) |
213 | 212 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) |
214 | 209, 213 | oveq12d 6567 |
. . . . . 6
⊢ (𝑗 = 𝑥 → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))))) |
215 | 214 | eleq1d 2672 |
. . . . 5
⊢ (𝑗 = 𝑥 → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
216 | 215 | cbvralv 3147 |
. . . 4
⊢
(∀𝑗 ∈
𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿) |
217 | 208, 216 | sylib 207 |
. . 3
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿) |
218 | | sseq2 3590 |
. . . . 5
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷))) |
219 | | xpeq2 5053 |
. . . . . . . . . 10
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))) |
220 | 219 | reseq2d 5317 |
. . . . . . . . 9
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))) |
221 | 220 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) |
222 | 221 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷)))))) |
223 | 222 | eleq1d 2672 |
. . . . . 6
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
224 | 223 | ralbidv 2969 |
. . . . 5
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → (∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) |
225 | 218, 224 | anbi12d 743 |
. . . 4
⊢ (𝑛 = (∪
ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿))) |
226 | 225 | rspcev 3282 |
. . 3
⊢ (((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ (∪ ran
𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran
𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿)) |
227 | 122, 124,
217, 226 | syl12anc 1316 |
. 2
⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿)) |
228 | 87, 227 | exlimddv 1850 |
1
⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿)) |