Step | Hyp | Ref
| Expression |
1 | | gsumzadd.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumzadd.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
3 | | gsumzadd.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
4 | 2, 3 | mndidcl 17694 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐵) |
6 | | gsumzadd.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
7 | 2, 6, 3 | mndlid 17697 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
8 | 1, 5, 7 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
9 | 8 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 ) |
10 | | gsumzaddlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
11 | | gsumzadd.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
12 | 3 | fvexi 6460 |
. . . . . . . . 9
⊢ 0 ∈
V |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ V) |
14 | | gsumzaddlem.h |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
15 | | fex 6761 |
. . . . . . . . . . 11
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
16 | 14, 11, 15 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ V) |
17 | 16 | suppun 7596 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
18 | | gsumzaddlem.w |
. . . . . . . . 9
⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 ) |
19 | 17, 18 | syl6sseqr 3871 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) |
20 | 10, 11, 13, 19 | gsumcllem 18695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 )) |
21 | 20 | oveq2d 6938 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
22 | 3 | gsumz 17760 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
23 | 1, 11, 22 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
24 | 23 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
25 | 21, 24 | eqtrd 2814 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 ) |
26 | | fex 6761 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
27 | 10, 11, 26 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
28 | 27 | suppun 7596 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 )) |
29 | | uncom 3980 |
. . . . . . . . . . 11
⊢ (𝐹 ∪ 𝐻) = (𝐻 ∪ 𝐹) |
30 | 29 | oveq1i 6932 |
. . . . . . . . . 10
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐻 ∪ 𝐹) supp 0 ) |
31 | 28, 30 | syl6sseqr 3871 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
32 | 31, 18 | syl6sseqr 3871 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊) |
33 | 14, 11, 13, 32 | gsumcllem 18695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻 = (𝑥 ∈ 𝐴 ↦ 0 )) |
34 | 33 | oveq2d 6938 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
35 | 34, 24 | eqtrd 2814 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 ) |
36 | 25, 35 | oveq12d 6940 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 )) |
37 | 11 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ 𝑉) |
38 | 5 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐵) |
39 | 37, 38, 38, 20, 33 | offval2 7191 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ 𝐴 ↦ ( 0 + 0 ))) |
40 | 9 | mpteq2dv 4980 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ ( 0 + 0 )) = (𝑥 ∈ 𝐴 ↦ 0 )) |
41 | 39, 40 | eqtrd 2814 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ 𝐴 ↦ 0 )) |
42 | 41 | oveq2d 6938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
43 | 42, 24 | eqtrd 2814 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = 0 ) |
44 | 9, 36, 43 | 3eqtr4rd 2825 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
45 | 44 | ex 403 |
. 2
⊢ (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
46 | 1 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐺 ∈ Mnd) |
47 | 2, 6 | mndcl 17687 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵) |
48 | 47 | 3expb 1110 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵) |
49 | 46, 48 | sylan 575 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵) |
50 | 49 | caovclg 7103 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
51 | | simprl 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (♯‘𝑊) ∈
ℕ) |
52 | | nnuz 12029 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
53 | 51, 52 | syl6eleq 2869 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (♯‘𝑊) ∈
(ℤ≥‘1)) |
54 | 10 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐹:𝐴⟶𝐵) |
55 | | f1of1 6390 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))–1-1→𝑊) |
56 | 55 | ad2antll 719 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1→𝑊) |
57 | | suppssdm 7589 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻)) |
59 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 = ((𝐹 ∪ 𝐻) supp 0 )) |
60 | | dmun 5576 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹 ∪ 𝐻) = (dom 𝐹 ∪ dom 𝐻) |
61 | 10 | fdmd 6300 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 = 𝐴) |
62 | 14 | fdmd 6300 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐻 = 𝐴) |
63 | 61, 62 | uneq12d 3991 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴 ∪ 𝐴)) |
64 | | unidm 3979 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
65 | 63, 64 | syl6eq 2830 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴) |
66 | 60, 65 | syl5req 2827 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = dom (𝐹 ∪ 𝐻)) |
67 | 58, 59, 66 | 3sstr4d 3867 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ⊆ 𝐴) |
68 | 67 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑊 ⊆ 𝐴) |
69 | | f1ss 6356 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝑊 ∧ 𝑊 ⊆ 𝐴) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴) |
70 | 56, 68, 69 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴) |
71 | | f1f 6351 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝑊))–1-1→𝐴 → 𝑓:(1...(♯‘𝑊))⟶𝐴) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))⟶𝐴) |
73 | | fco 6308 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
74 | 54, 72, 73 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
75 | 74 | ffvelrnda 6623 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
76 | 14 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐻:𝐴⟶𝐵) |
77 | | fco 6308 |
. . . . . . . . 9
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
78 | 76, 72, 77 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
79 | 78 | ffvelrnda 6623 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
80 | 54 | ffnd 6292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐹 Fn 𝐴) |
81 | 76 | ffnd 6292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐻 Fn 𝐴) |
82 | 11 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐴 ∈ 𝑉) |
83 | | ovexd 6956 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) →
(1...(♯‘𝑊))
∈ V) |
84 | | inidm 4043 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
85 | 80, 81, 72, 82, 82, 83, 84 | ofco 7194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) = ((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))) |
86 | 85 | fveq1d 6448 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘)) |
87 | 86 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘)) |
88 | | fnfco 6319 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
89 | 80, 72, 88 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
90 | | fnfco 6319 |
. . . . . . . . . 10
⊢ ((𝐻 Fn 𝐴 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
91 | 81, 72, 90 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
92 | | inidm 4043 |
. . . . . . . . 9
⊢
((1...(♯‘𝑊)) ∩ (1...(♯‘𝑊))) = (1...(♯‘𝑊)) |
93 | | eqidd 2779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = ((𝐹 ∘ 𝑓)‘𝑘)) |
94 | | eqidd 2779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
95 | 89, 91, 83, 83, 92, 93, 94 | ofval 7183 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘))) |
96 | 87, 95 | eqtrd 2814 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘))) |
97 | 1 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐺 ∈ Mnd) |
98 | | elfzouz 12793 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1..^(♯‘𝑊))
→ 𝑛 ∈
(ℤ≥‘1)) |
99 | 98 | adantl 475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈
(ℤ≥‘1)) |
100 | | elfzouz2 12803 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1..^(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝑛)) |
101 | 100 | adantl 475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (♯‘𝑊) ∈ (ℤ≥‘𝑛)) |
102 | | fzss2 12698 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝑛) → (1...𝑛) ⊆ (1...(♯‘𝑊))) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (1...𝑛) ⊆ (1...(♯‘𝑊))) |
104 | 103 | sselda 3821 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(♯‘𝑊))) |
105 | 75 | adantlr 705 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
106 | 104, 105 | syldan 585 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
107 | 2, 6 | mndcl 17687 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑘 + 𝑥) ∈ 𝐵) |
108 | 107 | 3expb 1110 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
109 | 97, 108 | sylan 575 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
110 | 99, 106, 109 | seqcl 13139 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑛) ∈ 𝐵) |
111 | 79 | adantlr 705 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
112 | 104, 111 | syldan 585 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
113 | 99, 112, 109 | seqcl 13139 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ 𝐵) |
114 | | fzofzp1 12884 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1..^(♯‘𝑊))
→ (𝑛 + 1) ∈
(1...(♯‘𝑊))) |
115 | | ffvelrn 6621 |
. . . . . . . . 9
⊢ (((𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
116 | 74, 114, 115 | syl2an 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
117 | | ffvelrn 6621 |
. . . . . . . . 9
⊢ (((𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
118 | 78, 114, 117 | syl2an 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
119 | | fvco3 6535 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
120 | 72, 114, 119 | syl2an 589 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
121 | | fveq2 6446 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹‘𝑘) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
122 | 121 | eleq1d 2844 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
123 | | gsumzaddlem.4 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
124 | 123 | expr 450 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑘 ∈ (𝐴 ∖ 𝑥) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
125 | 124 | ralrimiv 3147 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
126 | 125 | ex 403 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
127 | 126 | alrimiv 1970 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
128 | 127 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
129 | | imassrn 5731 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ (1...𝑛)) ⊆ ran 𝑓 |
130 | 72 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝐴) |
131 | 130 | frnd 6298 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝑓 ⊆ 𝐴) |
132 | 129, 131 | syl5ss 3832 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴) |
133 | | vex 3401 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
134 | 133 | imaex 7383 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ (1...𝑛)) ∈ V |
135 | | sseq1 3845 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴)) |
136 | | difeq2 3945 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛)))) |
137 | | reseq2 5637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻 ↾ 𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛)))) |
138 | 137 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻 ↾ 𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
139 | 138 | sneqd 4410 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻 ↾ 𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) |
140 | 139 | fveq2d 6450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
141 | 140 | eleq2d 2845 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
142 | 136, 141 | raleqbidv 3326 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
143 | 135, 142 | imbi12d 336 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))) |
144 | 134, 143 | spcv 3501 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
145 | 128, 132,
144 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
146 | | ffvelrn 6621 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴) |
147 | 72, 114, 146 | syl2an 589 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴) |
148 | | fzp1nel 12742 |
. . . . . . . . . . . . . 14
⊢ ¬
(𝑛 + 1) ∈ (1...𝑛) |
149 | 70 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴) |
150 | 114 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑛 + 1) ∈ (1...(♯‘𝑊))) |
151 | | f1elima 6792 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊)) ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛))) |
152 | 149, 150,
103, 151 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛))) |
153 | 148, 152 | mtbiri 319 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛))) |
154 | 147, 153 | eldifd 3803 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))) |
155 | 122, 145,
154 | rspcdva 3517 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
156 | 120, 155 | eqeltrd 2859 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
157 | | gsumzadd.z |
. . . . . . . . . . . . 13
⊢ 𝑍 = (Cntz‘𝐺) |
158 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V) |
159 | 14 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐻:𝐴⟶𝐵) |
160 | 159, 132 | fssresd 6321 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵) |
161 | | gsumzaddlem.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
162 | 161 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
163 | | resss 5671 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 |
164 | | rnss 5599 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) |
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ran
(𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻 |
166 | 157 | cntzidss 18153 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
167 | 162, 165,
166 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
168 | 99, 52 | syl6eleqr 2870 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ ℕ) |
169 | | f1ores 6405 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝐴 ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛))) |
170 | 149, 103,
169 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛))) |
171 | | f1of1 6390 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛))) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛))) |
173 | | suppssdm 7589 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛))) |
174 | | dmres 5668 |
. . . . . . . . . . . . . . . 16
⊢ dom
(𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)) |
176 | 173, 175 | syl5sseq 3872 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)) |
177 | | inss1 4053 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛)) |
178 | | df-ima 5368 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)) |
179 | 178 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))) |
180 | 177, 179 | syl5sseq 3872 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛))) |
181 | 176, 180 | sstrd 3831 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛))) |
182 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) |
183 | 2, 3, 6, 157, 97, 158, 160, 167, 168, 172, 181, 182 | gsumval3 18694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛)) |
184 | 178 | eqimss2i 3879 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) |
185 | | cores 5892 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
(𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))) |
186 | 184, 185 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))) |
187 | | resco 5893 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))) |
188 | 186, 187 | eqtr4i 2805 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) |
189 | 188 | fveq1i 6447 |
. . . . . . . . . . . . . . 15
⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) |
190 | | fvres 6465 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
191 | 189, 190 | syl5eq 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
192 | 191 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
193 | 99, 192 | seqfveq 13143 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) |
194 | 183, 193 | eqtr2d 2815 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
195 | | fvex 6459 |
. . . . . . . . . . . 12
⊢ (seq1(
+ ,
(𝐻 ∘ 𝑓))‘𝑛) ∈ V |
196 | 195 | elsn 4413 |
. . . . . . . . . . 11
⊢ ((seq1(
+ ,
(𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
197 | 194, 196 | sylibr 226 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) |
198 | 6, 157 | cntzi 18145 |
. . . . . . . . . 10
⊢ ((((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1)))) |
199 | 156, 197,
198 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1)))) |
200 | 199 | eqcomd 2784 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) = (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛))) |
201 | 2, 6, 97, 110, 113, 116, 118, 200 | mnd4g 17693 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) + (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1))))) |
202 | 50, 50, 53, 75, 79, 96, 201 | seqcaopr3 13154 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (seq1( + , ((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓))‘(♯‘𝑊)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊)))) |
203 | 49, 54, 76, 82, 82, 84 | off 7189 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝐵) |
204 | | gsumzaddlem.3 |
. . . . . . . 8
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
205 | 204 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
206 | 46, 108 | sylan 575 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
207 | 206, 54, 76, 82, 82, 84 | off 7189 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝐵) |
208 | | eldifi 3955 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥 ∈ 𝐴) |
209 | | eqidd 2779 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
210 | | eqidd 2779 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐻‘𝑥)) |
211 | 80, 81, 82, 82, 84, 209, 210 | ofval 7183 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥))) |
212 | 208, 211 | sylan2 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥))) |
213 | 17 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
214 | | f1ofo 6398 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))–onto→𝑊) |
215 | | forn 6369 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(1...(♯‘𝑊))–onto→𝑊 → ran 𝑓 = 𝑊) |
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = 𝑊) |
217 | 216, 18 | syl6eq 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = ((𝐹 ∪ 𝐻) supp 0 )) |
218 | 217 | sseq2d 3852 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
219 | 218 | ad2antll 719 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
220 | 213, 219 | mpbird 249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
221 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 0 ∈ V) |
222 | 54, 220, 82, 221 | suppssr 7608 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹‘𝑥) = 0 ) |
223 | 28 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 )) |
224 | 223, 30 | syl6sseqr 3871 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
225 | 217 | sseq2d 3852 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
226 | 225 | ad2antll 719 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
227 | 224, 226 | mpbird 249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓) |
228 | 76, 227, 82, 221 | suppssr 7608 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻‘𝑥) = 0 ) |
229 | 222, 228 | oveq12d 6940 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = ( 0 + 0 )) |
230 | 8 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 ) |
231 | 212, 229,
230 | 3eqtrd 2818 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = 0 ) |
232 | 207, 231 | suppss 7607 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓) |
233 | | ovex 6954 |
. . . . . . . . 9
⊢ (𝐹 ∘𝑓
+ 𝐻) ∈ V |
234 | 233, 133 | coex 7397 |
. . . . . . . 8
⊢ ((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) ∈ V |
235 | | suppimacnv 7587 |
. . . . . . . . 9
⊢ ((((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) supp 0 ) = (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 }))) |
236 | 235 | eqcomd 2784 |
. . . . . . . 8
⊢ ((((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) supp 0 )) |
237 | 234, 12, 236 | mp2an 682 |
. . . . . . 7
⊢ (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) supp 0 ) |
238 | 2, 3, 6, 157, 46, 82, 203, 205, 51, 70, 232, 237 | gsumval3 18694 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = (seq1( + , ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓))‘(♯‘𝑊))) |
239 | | gsumzaddlem.1 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
240 | 239 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
241 | | eqid 2778 |
. . . . . . . 8
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
242 | 2, 3, 6, 157, 46, 82, 54, 240, 51, 70, 220, 241 | gsumval3 18694 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))) |
243 | 161 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
244 | | eqid 2778 |
. . . . . . . 8
⊢ ((𝐻 ∘ 𝑓) supp 0 ) = ((𝐻 ∘ 𝑓) supp 0 ) |
245 | 2, 3, 6, 157, 46, 82, 76, 243, 51, 70, 227, 244 | gsumval3 18694 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊))) |
246 | 242, 245 | oveq12d 6940 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊)))) |
247 | 202, 238,
246 | 3eqtr4d 2824 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
248 | 247 | expr 450 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
249 | 248 | exlimdv 1976 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
250 | 249 | expimpd 447 |
. 2
⊢ (𝜑 → (((♯‘𝑊) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
251 | | gsumzadd.fn |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp 0 ) |
252 | | gsumzadd.hn |
. . . . 5
⊢ (𝜑 → 𝐻 finSupp 0 ) |
253 | 251, 252 | fsuppun 8582 |
. . . 4
⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ∈
Fin) |
254 | 18, 253 | syl5eqel 2863 |
. . 3
⊢ (𝜑 → 𝑊 ∈ Fin) |
255 | | fz1f1o 14848 |
. . 3
⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨
((♯‘𝑊) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊))) |
256 | 254, 255 | syl 17 |
. 2
⊢ (𝜑 → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊))) |
257 | 45, 250, 256 | mpjaod 849 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |