Step | Hyp | Ref
| Expression |
1 | | gsumzadd.b |
. 2
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsumzadd.0 |
. 2
⊢ 0 =
(0g‘𝐺) |
3 | | gsumzadd.p |
. 2
⊢ + =
(+g‘𝐺) |
4 | | gsumzadd.z |
. 2
⊢ 𝑍 = (Cntz‘𝐺) |
5 | | gsumzadd.g |
. 2
⊢ (𝜑 → 𝐺 ∈ Mnd) |
6 | | gsumzadd.a |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
7 | | gsumzadd.fn |
. 2
⊢ (𝜑 → 𝐹 finSupp 0 ) |
8 | | gsumzadd.hn |
. 2
⊢ (𝜑 → 𝐻 finSupp 0 ) |
9 | | eqid 2823 |
. 2
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐹 ∪ 𝐻) supp 0 ) |
10 | | gsumzadd.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
11 | | gsumzadd.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) |
12 | 1 | submss 17976 |
. . . 4
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ 𝐵) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
14 | 10, 13 | fssd 6530 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
15 | | gsumzadd.h |
. . 3
⊢ (𝜑 → 𝐻:𝐴⟶𝑆) |
16 | 15, 13 | fssd 6530 |
. 2
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
17 | | gsumzadd.c |
. . 3
⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑆)) |
18 | 10 | frnd 6523 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ 𝑆) |
19 | 4 | cntzidss 18470 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran 𝐹 ⊆ 𝑆) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
20 | 17, 18, 19 | syl2anc 586 |
. 2
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
21 | 15 | frnd 6523 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ 𝑆) |
22 | 4 | cntzidss 18470 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran 𝐻 ⊆ 𝑆) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
23 | 17, 21, 22 | syl2anc 586 |
. 2
⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
24 | 3 | submcl 17979 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
25 | 24 | 3expb 1116 |
. . . . . 6
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
26 | 11, 25 | sylan 582 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
27 | | inidm 4197 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
28 | 26, 10, 15, 6, 6, 27 | off 7426 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f + 𝐻):𝐴⟶𝑆) |
29 | 28 | frnd 6523 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘f + 𝐻) ⊆ 𝑆) |
30 | 4 | cntzidss 18470 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran (𝐹 ∘f + 𝐻) ⊆ 𝑆) → ran (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻))) |
31 | 17, 29, 30 | syl2anc 586 |
. 2
⊢ (𝜑 → ran (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻))) |
32 | 17 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ (𝑍‘𝑆)) |
33 | 13 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ 𝐵) |
34 | 5 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝐺 ∈ Mnd) |
35 | | vex 3499 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑥 ∈ V) |
37 | 11 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ∈ (SubMnd‘𝐺)) |
38 | | simpl 485 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥)) → 𝑥 ⊆ 𝐴) |
39 | | fssres 6546 |
. . . . . . . 8
⊢ ((𝐻:𝐴⟶𝑆 ∧ 𝑥 ⊆ 𝐴) → (𝐻 ↾ 𝑥):𝑥⟶𝑆) |
40 | 15, 38, 39 | syl2an 597 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 ↾ 𝑥):𝑥⟶𝑆) |
41 | 23 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
42 | | resss 5880 |
. . . . . . . . 9
⊢ (𝐻 ↾ 𝑥) ⊆ 𝐻 |
43 | 42 | rnssi 5812 |
. . . . . . . 8
⊢ ran
(𝐻 ↾ 𝑥) ⊆ ran 𝐻 |
44 | 4 | cntzidss 18470 |
. . . . . . . 8
⊢ ((ran
𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ 𝑥) ⊆ ran 𝐻) → ran (𝐻 ↾ 𝑥) ⊆ (𝑍‘ran (𝐻 ↾ 𝑥))) |
45 | 41, 43, 44 | sylancl 588 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ran (𝐻 ↾ 𝑥) ⊆ (𝑍‘ran (𝐻 ↾ 𝑥))) |
46 | 15 | ffund 6520 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐻) |
47 | | funres 6399 |
. . . . . . . . . 10
⊢ (Fun
𝐻 → Fun (𝐻 ↾ 𝑥)) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun (𝐻 ↾ 𝑥)) |
49 | 48 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → Fun (𝐻 ↾ 𝑥)) |
50 | 8 | fsuppimpd 8842 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ∈
Fin) |
51 | 50 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 supp 0 ) ∈
Fin) |
52 | | fex 6991 |
. . . . . . . . . . . 12
⊢ ((𝐻:𝐴⟶𝑆 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
53 | 15, 6, 52 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ V) |
54 | 2 | fvexi 6686 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
55 | | ressuppss 7851 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ V ∧ 0 ∈ V)
→ ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
56 | 53, 54, 55 | sylancl 588 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
57 | 56 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
58 | 51, 57 | ssfid 8743 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin) |
59 | | resfunexg 6980 |
. . . . . . . . . . 11
⊢ ((Fun
𝐻 ∧ 𝑥 ∈ V) → (𝐻 ↾ 𝑥) ∈ V) |
60 | 46, 35, 59 | sylancl 588 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 ↾ 𝑥) ∈ V) |
61 | | isfsupp 8839 |
. . . . . . . . . 10
⊢ (((𝐻 ↾ 𝑥) ∈ V ∧ 0 ∈ V) → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
62 | 60, 54, 61 | sylancl 588 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
63 | 62 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
64 | 49, 58, 63 | mpbir2and 711 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 ↾ 𝑥) finSupp 0 ) |
65 | 2, 4, 34, 36, 37, 40, 45, 64 | gsumzsubmcl 19040 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐺 Σg (𝐻 ↾ 𝑥)) ∈ 𝑆) |
66 | 65 | snssd 4744 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ 𝑆) |
67 | 1, 4 | cntz2ss 18465 |
. . . . 5
⊢ ((𝑆 ⊆ 𝐵 ∧ {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
68 | 33, 66, 67 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝑍‘𝑆) ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
69 | 32, 68 | sstrd 3979 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
70 | | eldifi 4105 |
. . . . 5
⊢ (𝑘 ∈ (𝐴 ∖ 𝑥) → 𝑘 ∈ 𝐴) |
71 | 70 | adantl 484 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥)) → 𝑘 ∈ 𝐴) |
72 | | ffvelrn 6851 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑆 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝑆) |
73 | 10, 71, 72 | syl2an 597 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ 𝑆) |
74 | 69, 73 | sseldd 3970 |
. 2
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
75 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 14,
16, 20, 23, 31, 74 | gsumzaddlem 19043 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |