Step | Hyp | Ref
| Expression |
1 | | gsumzadd.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumzadd.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
3 | | gsumzadd.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
4 | 2, 3 | mndidcl 17131 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ 𝐵) |
6 | | gsumzadd.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
7 | 2, 6, 3 | mndlid 17134 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
8 | 1, 5, 7 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ( 0 + 0 ) = 0 ) |
9 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 ) |
10 | | gsumzaddlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
11 | | gsumzadd.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
12 | | fvex 6113 |
. . . . . . . . . 10
⊢
(0g‘𝐺) ∈ V |
13 | 3, 12 | eqeltri 2684 |
. . . . . . . . 9
⊢ 0 ∈
V |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ V) |
15 | | gsumzaddlem.h |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
16 | | fex 6394 |
. . . . . . . . . . 11
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
17 | 15, 11, 16 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ V) |
18 | 17 | suppun 7202 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
19 | | gsumzaddlem.w |
. . . . . . . . 9
⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 ) |
20 | 18, 19 | syl6sseqr 3615 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) |
21 | 10, 11, 14, 20 | gsumcllem 18132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 )) |
22 | 21 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
23 | 3 | gsumz 17197 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
24 | 1, 11, 23 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 ) |
26 | 22, 25 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 ) |
27 | | fex 6394 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
28 | 10, 11, 27 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
29 | 28 | suppun 7202 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 )) |
30 | | uncom 3719 |
. . . . . . . . . . 11
⊢ (𝐹 ∪ 𝐻) = (𝐻 ∪ 𝐹) |
31 | 30 | oveq1i 6559 |
. . . . . . . . . 10
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐻 ∪ 𝐹) supp 0 ) |
32 | 29, 31 | syl6sseqr 3615 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
33 | 32, 19 | syl6sseqr 3615 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊) |
34 | 15, 11, 14, 33 | gsumcllem 18132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻 = (𝑥 ∈ 𝐴 ↦ 0 )) |
35 | 34 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
36 | 35, 25 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 ) |
37 | 26, 36 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 )) |
38 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ 𝑉) |
39 | 5 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐵) |
40 | 38, 39, 39, 21, 34 | offval2 6812 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ 𝐴 ↦ ( 0 + 0 ))) |
41 | 9 | mpteq2dv 4673 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ ( 0 + 0 )) = (𝑥 ∈ 𝐴 ↦ 0 )) |
42 | 40, 41 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ 𝐴 ↦ 0 )) |
43 | 42 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 ))) |
44 | 43, 25 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = 0 ) |
45 | 9, 37, 44 | 3eqtr4rd 2655 |
. . 3
⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
46 | 45 | ex 449 |
. 2
⊢ (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
47 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐺 ∈ Mnd) |
48 | 2, 6 | mndcl 17124 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵) |
49 | 48 | 3expb 1258 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵) |
50 | 47, 49 | sylan 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵) |
51 | 50 | caovclg 6724 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
52 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (#‘𝑊) ∈
ℕ) |
53 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
54 | 52, 53 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (#‘𝑊) ∈
(ℤ≥‘1)) |
55 | 10 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐹:𝐴⟶𝐵) |
56 | | f1of1 6049 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(#‘𝑊))–1-1→𝑊) |
57 | 56 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))–1-1→𝑊) |
58 | | suppssdm 7195 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻) |
59 | 58 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻)) |
60 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 = ((𝐹 ∪ 𝐻) supp 0 )) |
61 | | dmun 5253 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐹 ∪ 𝐻) = (dom 𝐹 ∪ dom 𝐻) |
62 | | fdm 5964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
63 | 10, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 = 𝐴) |
64 | | fdm 5964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻:𝐴⟶𝐵 → dom 𝐻 = 𝐴) |
65 | 15, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐻 = 𝐴) |
66 | 63, 65 | uneq12d 3730 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴 ∪ 𝐴)) |
67 | | unidm 3718 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
68 | 66, 67 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴) |
69 | 61, 68 | syl5req 2657 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = dom (𝐹 ∪ 𝐻)) |
70 | 59, 60, 69 | 3sstr4d 3611 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ⊆ 𝐴) |
71 | 70 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑊 ⊆ 𝐴) |
72 | | f1ss 6019 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(#‘𝑊))–1-1→𝑊 ∧ 𝑊 ⊆ 𝐴) → 𝑓:(1...(#‘𝑊))–1-1→𝐴) |
73 | 57, 71, 72 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))–1-1→𝐴) |
74 | | f1f 6014 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝑊))–1-1→𝐴 → 𝑓:(1...(#‘𝑊))⟶𝐴) |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))⟶𝐴) |
76 | | fco 5971 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵) |
77 | 55, 75, 76 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵) |
78 | 77 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
79 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐻:𝐴⟶𝐵) |
80 | | fco 5971 |
. . . . . . . . 9
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵) |
81 | 79, 75, 80 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵) |
82 | 81 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
83 | 55 | ffnd 5959 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐹 Fn 𝐴) |
84 | 79 | ffnd 5959 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐻 Fn 𝐴) |
85 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐴 ∈ 𝑉) |
86 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
(1...(#‘𝑊))
∈ V |
87 | 86 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (1...(#‘𝑊)) ∈ V) |
88 | | inidm 3784 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
89 | 83, 84, 75, 85, 85, 87, 88 | ofco 6815 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) = ((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))) |
90 | 89 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘)) |
91 | 90 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘)) |
92 | | fnfco 5982 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓) Fn (1...(#‘𝑊))) |
93 | 83, 75, 92 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓) Fn (1...(#‘𝑊))) |
94 | | fnfco 5982 |
. . . . . . . . . 10
⊢ ((𝐻 Fn 𝐴 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓) Fn (1...(#‘𝑊))) |
95 | 84, 75, 94 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓) Fn (1...(#‘𝑊))) |
96 | | inidm 3784 |
. . . . . . . . 9
⊢
((1...(#‘𝑊))
∩ (1...(#‘𝑊))) =
(1...(#‘𝑊)) |
97 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = ((𝐹 ∘ 𝑓)‘𝑘)) |
98 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
99 | 93, 95, 87, 87, 96, 97, 98 | ofval 6804 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘))) |
100 | 91, 99 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘))) |
101 | 1 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐺 ∈ Mnd) |
102 | | elfzouz 12343 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1..^(#‘𝑊)) → 𝑛 ∈
(ℤ≥‘1)) |
103 | 102 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈
(ℤ≥‘1)) |
104 | | elfzouz2 12353 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1..^(#‘𝑊)) → (#‘𝑊) ∈
(ℤ≥‘𝑛)) |
105 | 104 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ∈ (ℤ≥‘𝑛)) |
106 | | fzss2 12252 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
(ℤ≥‘𝑛) → (1...𝑛) ⊆ (1...(#‘𝑊))) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (1...𝑛) ⊆ (1...(#‘𝑊))) |
108 | 107 | sselda 3568 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(#‘𝑊))) |
109 | 78 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
110 | 108, 109 | syldan 486 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
111 | 2, 6 | mndcl 17124 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑘 + 𝑥) ∈ 𝐵) |
112 | 111 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
113 | 101, 112 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
114 | 103, 110,
113 | seqcl 12683 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑛) ∈ 𝐵) |
115 | 82 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
116 | 108, 115 | syldan 486 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵) |
117 | 103, 116,
113 | seqcl 12683 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ 𝐵) |
118 | | fzofzp1 12431 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1..^(#‘𝑊)) → (𝑛 + 1) ∈ (1...(#‘𝑊))) |
119 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ (((𝐹 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
120 | 77, 118, 119 | syl2an 493 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
121 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ (((𝐻 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
122 | 81, 118, 121 | syl2an 493 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵) |
123 | | fvco3 6185 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
124 | 75, 118, 123 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
125 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹‘𝑘) = (𝐹‘(𝑓‘(𝑛 + 1)))) |
126 | 125 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
127 | | gsumzaddlem.4 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
128 | 127 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑘 ∈ (𝐴 ∖ 𝑥) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
129 | 128 | ralrimiv 2948 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
130 | 129 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
131 | 130 | alrimiv 1842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
132 | 131 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))) |
133 | | imassrn 5396 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ (1...𝑛)) ⊆ ran 𝑓 |
134 | 75 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝐴) |
135 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(#‘𝑊))⟶𝐴 → ran 𝑓 ⊆ 𝐴) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝑓 ⊆ 𝐴) |
137 | 133, 136 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴) |
138 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
139 | 138 | imaex 6996 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ (1...𝑛)) ∈ V |
140 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴)) |
141 | | difeq2 3684 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛)))) |
142 | | reseq2 5312 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻 ↾ 𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛)))) |
143 | 142 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻 ↾ 𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
144 | 143 | sneqd 4137 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻 ↾ 𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) |
145 | 144 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
146 | 145 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
147 | 141, 146 | raleqbidv 3129 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
148 | 140, 147 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))) |
149 | 139, 148 | spcv 3272 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))) |
150 | 132, 137,
149 | sylc 63 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
151 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴) |
152 | 75, 118, 151 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴) |
153 | | fzp1nel 12293 |
. . . . . . . . . . . . . 14
⊢ ¬
(𝑛 + 1) ∈ (1...𝑛) |
154 | 73 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))–1-1→𝐴) |
155 | 118 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑛 + 1) ∈ (1...(#‘𝑊))) |
156 | | f1elima 6421 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(#‘𝑊))–1-1→𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊)) ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛))) |
157 | 154, 155,
107, 156 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛))) |
158 | 153, 157 | mtbiri 316 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛))) |
159 | 152, 158 | eldifd 3551 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))) |
160 | 126, 150,
159 | rspcdva 3288 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
161 | 124, 160 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})) |
162 | | gsumzadd.z |
. . . . . . . . . . . . 13
⊢ 𝑍 = (Cntz‘𝐺) |
163 | 139 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V) |
164 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐻:𝐴⟶𝐵) |
165 | 164, 137 | fssresd 5984 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵) |
166 | | gsumzaddlem.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
167 | 166 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
168 | | resss 5342 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 |
169 | | rnss 5275 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) |
170 | 168, 169 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ran
(𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻 |
171 | 162 | cntzidss 17593 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
172 | 167, 170,
171 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
173 | 103, 53 | syl6eleqr 2699 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ ℕ) |
174 | | f1ores 6064 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(#‘𝑊))–1-1→𝐴 ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛))) |
175 | 154, 107,
174 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛))) |
176 | | f1of1 6049 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛))) |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛))) |
178 | | suppssdm 7195 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛))) |
179 | | dmres 5339 |
. . . . . . . . . . . . . . . 16
⊢ dom
(𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)) |
181 | 178, 180 | syl5sseq 3616 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)) |
182 | | inss1 3795 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛)) |
183 | | df-ima 5051 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)) |
184 | 183 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))) |
185 | 182, 184 | syl5sseq 3616 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛))) |
186 | 181, 185 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛))) |
187 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) |
188 | 2, 3, 6, 162, 101, 163, 165, 172, 173, 177, 186, 187 | gsumval3 18131 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛)) |
189 | 183 | eqimss2i 3623 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) |
190 | | cores 5555 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
(𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))) |
191 | 189, 190 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))) |
192 | | resco 5556 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))) |
193 | 191, 192 | eqtr4i 2635 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) |
194 | 193 | fveq1i 6104 |
. . . . . . . . . . . . . . 15
⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) |
195 | | fvres 6117 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
196 | 194, 195 | syl5eq 2656 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
197 | 196 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘)) |
198 | 103, 197 | seqfveq 12687 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) |
199 | 188, 198 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
200 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (seq1(
+ ,
(𝐻 ∘ 𝑓))‘𝑛) ∈ V |
201 | 200 | elsn 4140 |
. . . . . . . . . . 11
⊢ ((seq1(
+ ,
(𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))) |
202 | 199, 201 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) |
203 | 6, 162 | cntzi 17585 |
. . . . . . . . . 10
⊢ ((((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1)))) |
204 | 161, 202,
203 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1)))) |
205 | 204 | eqcomd 2616 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) = (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛))) |
206 | 2, 6, 101, 114, 117, 120, 122, 205 | mnd4g 17130 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) + (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1))))) |
207 | 51, 51, 54, 78, 82, 100, 206 | seqcaopr3 12698 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (seq1( + , ((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓))‘(#‘𝑊)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(#‘𝑊)))) |
208 | 50, 55, 79, 85, 85, 88 | off 6810 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝐵) |
209 | | gsumzaddlem.3 |
. . . . . . . 8
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
210 | 209 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
211 | 47, 112 | sylan 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵) |
212 | 211, 55, 79, 85, 85, 88 | off 6810 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝐵) |
213 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥 ∈ 𝐴) |
214 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
215 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐻‘𝑥)) |
216 | 83, 84, 85, 85, 88, 214, 215 | ofval 6804 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥))) |
217 | 213, 216 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥))) |
218 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
219 | | f1ofo 6057 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(#‘𝑊))–onto→𝑊) |
220 | | forn 6031 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(1...(#‘𝑊))–onto→𝑊 → ran 𝑓 = 𝑊) |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = 𝑊) |
222 | 221, 19 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = ((𝐹 ∪ 𝐻) supp 0 )) |
223 | 222 | sseq2d 3596 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
224 | 223 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
225 | 218, 224 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
226 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 0 ∈ V) |
227 | 55, 225, 85, 226 | suppssr 7213 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹‘𝑥) = 0 ) |
228 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 )) |
229 | 228, 31 | syl6sseqr 3615 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )) |
230 | 222 | sseq2d 3596 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
231 | 230 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))) |
232 | 229, 231 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓) |
233 | 79, 232, 85, 226 | suppssr 7213 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻‘𝑥) = 0 ) |
234 | 227, 233 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = ( 0 + 0 )) |
235 | 8 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 ) |
236 | 217, 234,
235 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = 0 ) |
237 | 212, 236 | suppss 7212 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓) |
238 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝐹 ∘𝑓
+ 𝐻) ∈ V |
239 | 238, 138 | coex 7011 |
. . . . . . . 8
⊢ ((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) ∈ V |
240 | | suppimacnv 7193 |
. . . . . . . . 9
⊢ ((((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) supp 0 ) = (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 }))) |
241 | 240 | eqcomd 2616 |
. . . . . . . 8
⊢ ((((𝐹 ∘𝑓
+ 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) supp 0 )) |
242 | 239, 13, 241 | mp2an 704 |
. . . . . . 7
⊢ (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) supp 0 ) |
243 | 2, 3, 6, 162, 47, 85, 208, 210, 52, 73, 237, 242 | gsumval3 18131 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = (seq1( + , ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊))) |
244 | | gsumzaddlem.1 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
245 | 244 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
246 | | eqid 2610 |
. . . . . . . 8
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
247 | 2, 3, 6, 162, 47, 85, 55, 245, 52, 73, 225, 246 | gsumval3 18131 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))) |
248 | 166 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
249 | | eqid 2610 |
. . . . . . . 8
⊢ ((𝐻 ∘ 𝑓) supp 0 ) = ((𝐻 ∘ 𝑓) supp 0 ) |
250 | 2, 3, 6, 162, 47, 85, 79, 248, 52, 73, 232, 249 | gsumval3 18131 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻 ∘ 𝑓))‘(#‘𝑊))) |
251 | 247, 250 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(#‘𝑊)))) |
252 | 207, 243,
251 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
253 | 252 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
254 | 253 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
255 | 254 | expimpd 627 |
. 2
⊢ (𝜑 → (((#‘𝑊) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊) → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) |
256 | | gsumzadd.fn |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp 0 ) |
257 | | gsumzadd.hn |
. . . . 5
⊢ (𝜑 → 𝐻 finSupp 0 ) |
258 | 256, 257 | fsuppun 8177 |
. . . 4
⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ∈
Fin) |
259 | 19, 258 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝑊 ∈ Fin) |
260 | | fz1f1o 14288 |
. . 3
⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))) |
261 | 259, 260 | syl 17 |
. 2
⊢ (𝜑 → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))) |
262 | 46, 255, 261 | mpjaod 395 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |