Step | Hyp | Ref
| Expression |
1 | | gsumzadd.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumzadd.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
3 | | gsumzadd.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
4 | 2, 3 | mndidcl 17926 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐵) |
6 | | gsumzadd.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
7 | 2, 6, 3 | mndlid 17931 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
8 | 1, 5, 7 | syl2anc 586 |
. . . . 5
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
9 | 8 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 ) |
10 | | gsumzaddlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
11 | | gsumzadd.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
12 | 3 | fvexi 6684 |
. . . . . . . . 9
⊢ 0 ∈
V |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ V) |
14 | | gsumzaddlem.h |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
15 | | fex 6989 |
. . . . . . . . . . 11
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
16 | 14, 11, 15 | syl2anc 586 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ V) |
17 | 16 | suppun 7850 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
18 | | gsumzaddlem.w |
. . . . . . . . 9
⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 ) |
19 | 17, 18 | sseqtrrdi 4018 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) |
20 | 10, 11, 13, 19 | gsumcllem 19028 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 )) |
21 | 20 | oveq2d 7172 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
22 | 3 | gsumz 18000 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
23 | 1, 11, 22 | syl2anc 586 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
24 | 23 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
25 | 21, 24 | eqtrd 2856 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 ) |
26 | | fex 6989 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
27 | 10, 11, 26 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
28 | 27 | suppun 7850 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 )) |
29 | | uncom 4129 |
. . . . . . . . . . 11
⊢ (𝐹 ∪ 𝐻) = (𝐻 ∪ 𝐹) |
30 | 29 | oveq1i 7166 |
. . . . . . . . . 10
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐻 ∪ 𝐹) supp 0 ) |
31 | 28, 30 | sseqtrrdi 4018 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
32 | 31, 18 | sseqtrrdi 4018 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊) |
33 | 14, 11, 13, 32 | gsumcllem 19028 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻 = (𝑥 ∈ 𝐴 ↦ 0 )) |
34 | 33 | oveq2d 7172 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
35 | 34, 24 | eqtrd 2856 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 ) |
36 | 25, 35 | oveq12d 7174 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 )) |
37 | 11 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ 𝑉) |
38 | 5 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐵) |
39 | 37, 38, 38, 20, 33 | offval2 7426 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘f + 𝐻) = (𝑥 ∈ 𝐴 ↦ ( 0 + 0 ))) |
40 | 9 | mpteq2dv 5162 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ ( 0 + 0 )) = (𝑥 ∈ 𝐴 ↦ 0 )) |
41 | 39, 40 | eqtrd 2856 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘f + 𝐻) = (𝑥 ∈ 𝐴 ↦ 0 )) |
42 | 41 | oveq2d 7172 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
43 | 42, 24 | eqtrd 2856 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = 0 ) |
44 | 9, 36, 43 | 3eqtr4rd 2867 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
45 | 44 | ex 415 |
. 2
⊢ (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
46 | 1 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐺 ∈ Mnd) |
47 | 2, 6 | mndcl 17919 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵) |
48 | 47 | 3expb 1116 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵) |
49 | 46, 48 | sylan 582 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵) |
50 | 49 | caovclg 7340 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
51 | | simprl 769 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (♯‘𝑊) ∈
ℕ) |
52 | | nnuz 12282 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
53 | 51, 52 | eleqtrdi 2923 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (♯‘𝑊) ∈
(ℤ≥‘1)) |
54 | 10 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐹:𝐴⟶𝐵) |
55 | | f1of1 6614 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))–1-1→𝑊) |
56 | 55 | ad2antll 727 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1→𝑊) |
57 | | suppssdm 7843 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻)) |
59 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 = ((𝐹 ∪ 𝐻) supp 0 )) |
60 | | dmun 5779 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹 ∪ 𝐻) = (dom 𝐹 ∪ dom 𝐻) |
61 | 10 | fdmd 6523 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 = 𝐴) |
62 | 14 | fdmd 6523 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐻 = 𝐴) |
63 | 61, 62 | uneq12d 4140 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴 ∪ 𝐴)) |
64 | | unidm 4128 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
65 | 63, 64 | syl6eq 2872 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴) |
66 | 60, 65 | syl5req 2869 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = dom (𝐹 ∪ 𝐻)) |
67 | 58, 59, 66 | 3sstr4d 4014 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ⊆ 𝐴) |
68 | 67 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑊 ⊆ 𝐴) |
69 | | f1ss 6580 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝑊 ∧ 𝑊 ⊆ 𝐴) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴) |
70 | 56, 68, 69 | syl2anc 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴) |
71 | | f1f 6575 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝑊))–1-1→𝐴 → 𝑓:(1...(♯‘𝑊))⟶𝐴) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))⟶𝐴) |
73 | | fco 6531 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
74 | 54, 72, 73 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
75 | 74 | ffvelrnda 6851 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
76 | 14 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐻:𝐴⟶𝐵) |
77 | | fco 6531 |
. . . . . . . . 9
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
78 | 76, 72, 77 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵) |
79 | 78 | ffvelrnda 6851 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
80 | 54 | ffnd 6515 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐹 Fn 𝐴) |
81 | 76 | ffnd 6515 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐻 Fn 𝐴) |
82 | 11 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐴 ∈ 𝑉) |
83 | | ovexd 7191 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) →
(1...(♯‘𝑊))
∈ V) |
84 | | inidm 4195 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
85 | 80, 81, 72, 82, 82, 83, 84 | ofco 7429 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘f + 𝐻) ∘ 𝑓) = ((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))) |
86 | 85 | fveq1d 6672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (((𝐹 ∘f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))‘𝑘)) |
87 | 86 | adantr 483 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))‘𝑘)) |
88 | | fnfco 6543 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
89 | 80, 72, 88 | syl2anc 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
90 | | fnfco 6543 |
. . . . . . . . . 10
⊢ ((𝐻 Fn 𝐴 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
91 | 81, 72, 90 | syl2anc 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓) Fn (1...(♯‘𝑊))) |
92 | | inidm 4195 |
. . . . . . . . 9
⊢
((1...(♯‘𝑊)) ∩ (1...(♯‘𝑊))) = (1...(♯‘𝑊)) |
93 | | eqidd 2822 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = ((𝐹 ∘ 𝑓)‘𝑘)) |
94 | | eqidd 2822 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
95 | 89, 91, 83, 83, 92, 93, 94 | ofval 7418 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘))) |
96 | 87, 95 | eqtrd 2856 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘))) |
97 | 1 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐺 ∈ Mnd) |
98 | | elfzouz 13043 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1..^(♯‘𝑊))
→ 𝑛 ∈
(ℤ≥‘1)) |
99 | 98 | adantl 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈
(ℤ≥‘1)) |
100 | | elfzouz2 13053 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1..^(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝑛)) |
101 | 100 | adantl 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (♯‘𝑊) ∈ (ℤ≥‘𝑛)) |
102 | | fzss2 12948 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝑛) → (1...𝑛) ⊆ (1...(♯‘𝑊))) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (1...𝑛) ⊆ (1...(♯‘𝑊))) |
104 | 103 | sselda 3967 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(♯‘𝑊))) |
105 | 75 | adantlr 713 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
106 | 104, 105 | syldan 593 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
107 | 2, 6 | mndcl 17919 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑘 + 𝑥) ∈ 𝐵) |
108 | 107 | 3expb 1116 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
109 | 97, 108 | sylan 582 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
110 | 99, 106, 109 | seqcl 13391 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑛) ∈ 𝐵) |
111 | 79 | adantlr 713 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
112 | 104, 111 | syldan 593 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
113 | 99, 112, 109 | seqcl 13391 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ 𝐵) |
114 | | fzofzp1 13135 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1..^(♯‘𝑊))
→ (𝑛 + 1) ∈
(1...(♯‘𝑊))) |
115 | | ffvelrn 6849 |
. . . . . . . . 9
⊢ (((𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
116 | 74, 114, 115 | syl2an 597 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
117 | | ffvelrn 6849 |
. . . . . . . . 9
⊢ (((𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
118 | 78, 114, 117 | syl2an 597 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
119 | | fvco3 6760 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
120 | 72, 114, 119 | syl2an 597 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
121 | | fveq2 6670 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹‘𝑘) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
122 | 121 | eleq1d 2897 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
123 | | gsumzaddlem.4 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
124 | 123 | expr 459 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑘 ∈ (𝐴 ∖ 𝑥) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
125 | 124 | ralrimiv 3181 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
126 | 125 | ex 415 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
127 | 126 | alrimiv 1928 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
128 | 127 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
129 | | imassrn 5940 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ (1...𝑛)) ⊆ ran 𝑓 |
130 | 72 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝐴) |
131 | 130 | frnd 6521 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝑓 ⊆ 𝐴) |
132 | 129, 131 | sstrid 3978 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴) |
133 | | vex 3497 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
134 | 133 | imaex 7621 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ (1...𝑛)) ∈ V |
135 | | sseq1 3992 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴)) |
136 | | difeq2 4093 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛)))) |
137 | | reseq2 5848 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻 ↾ 𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛)))) |
138 | 137 | oveq2d 7172 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻 ↾ 𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
139 | 138 | sneqd 4579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻 ↾ 𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) |
140 | 139 | fveq2d 6674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
141 | 140 | eleq2d 2898 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
142 | 136, 141 | raleqbidv 3401 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
143 | 135, 142 | imbi12d 347 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))) |
144 | 134, 143 | spcv 3606 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
145 | 128, 132,
144 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
146 | | ffvelrn 6849 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴) |
147 | 72, 114, 146 | syl2an 597 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴) |
148 | | fzp1nel 12992 |
. . . . . . . . . . . . . 14
⊢ ¬
(𝑛 + 1) ∈ (1...𝑛) |
149 | 70 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴) |
150 | 114 | adantl 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑛 + 1) ∈ (1...(♯‘𝑊))) |
151 | | f1elima 7021 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊)) ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛))) |
152 | 149, 150,
103, 151 | syl3anc 1367 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛))) |
153 | 148, 152 | mtbiri 329 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛))) |
154 | 147, 153 | eldifd 3947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))) |
155 | 122, 145,
154 | rspcdva 3625 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
156 | 120, 155 | eqeltrd 2913 |
. . . . . . . . . 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 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐻:𝐴⟶𝐵) |
160 | 159, 132 | fssresd 6545 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵) |
161 | | gsumzaddlem.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
162 | 161 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
163 | | resss 5878 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 |
164 | 163 | rnssi 5810 |
. . . . . . . . . . . . . 14
⊢ ran
(𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻 |
165 | 157 | cntzidss 18468 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
166 | 162, 164,
165 | sylancl 588 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
167 | 99, 52 | eleqtrrdi 2924 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ ℕ) |
168 | | f1ores 6629 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝐴 ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛))) |
169 | 149, 103,
168 | syl2anc 586 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛))) |
170 | | f1of1 6614 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛))) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛))) |
172 | | suppssdm 7843 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛))) |
173 | | dmres 5875 |
. . . . . . . . . . . . . . . 16
⊢ dom
(𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) |
174 | 173 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)) |
175 | 172, 174 | sseqtrid 4019 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)) |
176 | | inss1 4205 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛)) |
177 | | df-ima 5568 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)) |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))) |
179 | 176, 178 | sseqtrid 4019 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛))) |
180 | 175, 179 | sstrd 3977 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛))) |
181 | | eqid 2821 |
. . . . . . . . . . . . 13
⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) |
182 | 2, 3, 6, 157, 97, 158, 160, 166, 167, 171, 180, 181 | gsumval3 19027 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛)) |
183 | 177 | eqimss2i 4026 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) |
184 | | cores 6102 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
(𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))) |
185 | 183, 184 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))) |
186 | | resco 6103 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))) |
187 | 185, 186 | eqtr4i 2847 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) |
188 | 187 | fveq1i 6671 |
. . . . . . . . . . . . . . 15
⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) |
189 | | fvres 6689 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
190 | 188, 189 | syl5eq 2868 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
191 | 190 | adantl 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
192 | 99, 191 | seqfveq 13395 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) |
193 | 182, 192 | eqtr2d 2857 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
194 | | fvex 6683 |
. . . . . . . . . . . 12
⊢ (seq1(
+ ,
(𝐻 ∘ 𝑓))‘𝑛) ∈ V |
195 | 194 | elsn 4582 |
. . . . . . . . . . 11
⊢ ((seq1(
+ ,
(𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
196 | 193, 195 | sylibr 236 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) |
197 | 6, 157 | cntzi 18459 |
. . . . . . . . . 10
⊢ ((((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1)))) |
198 | 156, 196,
197 | syl2anc 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1)))) |
199 | 198 | eqcomd 2827 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) = (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛))) |
200 | 2, 6, 97, 110, 113, 116, 118, 199 | mnd4g 17925 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) + (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1))))) |
201 | 50, 50, 53, 75, 79, 96, 200 | seqcaopr3 13406 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (seq1( + , ((𝐹 ∘f + 𝐻) ∘ 𝑓))‘(♯‘𝑊)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊)))) |
202 | 49, 54, 76, 82, 82, 84 | off 7424 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘f + 𝐻):𝐴⟶𝐵) |
203 | | gsumzaddlem.3 |
. . . . . . . 8
⊢ (𝜑 → ran (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻))) |
204 | 203 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻))) |
205 | 46, 108 | sylan 582 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
206 | 205, 54, 76, 82, 82, 84 | off 7424 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘f + 𝐻):𝐴⟶𝐵) |
207 | | eldifi 4103 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥 ∈ 𝐴) |
208 | | eqidd 2822 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
209 | | eqidd 2822 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐻‘𝑥)) |
210 | 80, 81, 82, 82, 84, 208, 209 | ofval 7418 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘f + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥))) |
211 | 207, 210 | sylan2 594 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘f + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥))) |
212 | 17 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
213 | | f1ofo 6622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))–onto→𝑊) |
214 | | forn 6593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(1...(♯‘𝑊))–onto→𝑊 → ran 𝑓 = 𝑊) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = 𝑊) |
216 | 215, 18 | syl6eq 2872 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = ((𝐹 ∪ 𝐻) supp 0 )) |
217 | 216 | sseq2d 3999 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
218 | 217 | ad2antll 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
219 | 212, 218 | mpbird 259 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
220 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 0 ∈ V) |
221 | 54, 219, 82, 220 | suppssr 7861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹‘𝑥) = 0 ) |
222 | 28 | adantr 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 )) |
223 | 222, 30 | sseqtrrdi 4018 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
224 | 216 | sseq2d 3999 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
225 | 224 | ad2antll 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
226 | 223, 225 | mpbird 259 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓) |
227 | 76, 226, 82, 220 | suppssr 7861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻‘𝑥) = 0 ) |
228 | 221, 227 | oveq12d 7174 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = ( 0 + 0 )) |
229 | 8 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 ) |
230 | 211, 228,
229 | 3eqtrd 2860 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘f + 𝐻)‘𝑥) = 0 ) |
231 | 206, 230 | suppss 7860 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘f + 𝐻) supp 0 ) ⊆ ran 𝑓) |
232 | | ovex 7189 |
. . . . . . . . 9
⊢ (𝐹 ∘f + 𝐻) ∈ V |
233 | 232, 133 | coex 7635 |
. . . . . . . 8
⊢ ((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V |
234 | | suppimacnv 7841 |
. . . . . . . . 9
⊢ ((((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹 ∘f + 𝐻) ∘ 𝑓) supp 0 ) = (◡((𝐹 ∘f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 }))) |
235 | 234 | eqcomd 2827 |
. . . . . . . 8
⊢ ((((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (◡((𝐹 ∘f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘f + 𝐻) ∘ 𝑓) supp 0 )) |
236 | 233, 12, 235 | mp2an 690 |
. . . . . . 7
⊢ (◡((𝐹 ∘f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘f + 𝐻) ∘ 𝑓) supp 0 ) |
237 | 2, 3, 6, 157, 46, 82, 202, 204, 51, 70, 231, 236 | gsumval3 19027 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = (seq1( + , ((𝐹 ∘f + 𝐻) ∘ 𝑓))‘(♯‘𝑊))) |
238 | | gsumzaddlem.1 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
239 | 238 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
240 | | eqid 2821 |
. . . . . . . 8
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
241 | 2, 3, 6, 157, 46, 82, 54, 239, 51, 70, 219, 240 | gsumval3 19027 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))) |
242 | 161 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
243 | | eqid 2821 |
. . . . . . . 8
⊢ ((𝐻 ∘ 𝑓) supp 0 ) = ((𝐻 ∘ 𝑓) supp 0 ) |
244 | 2, 3, 6, 157, 46, 82, 76, 242, 51, 70, 226, 243 | gsumval3 19027 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊))) |
245 | 241, 244 | oveq12d 7174 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊)))) |
246 | 201, 237,
245 | 3eqtr4d 2866 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
247 | 246 | expr 459 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
248 | 247 | exlimdv 1934 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
249 | 248 | expimpd 456 |
. 2
⊢ (𝜑 → (((♯‘𝑊) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
250 | | gsumzadd.fn |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp 0 ) |
251 | | gsumzadd.hn |
. . . . 5
⊢ (𝜑 → 𝐻 finSupp 0 ) |
252 | 250, 251 | fsuppun 8852 |
. . . 4
⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ∈
Fin) |
253 | 18, 252 | eqeltrid 2917 |
. . 3
⊢ (𝜑 → 𝑊 ∈ Fin) |
254 | | fz1f1o 15067 |
. . 3
⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨
((♯‘𝑊) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊))) |
255 | 253, 254 | syl 17 |
. 2
⊢ (𝜑 → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊))) |
256 | 45, 249, 255 | mpjaod 856 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |