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 2777 |
. 2
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐹 ∪ 𝐻) supp 0 ) |
10 | | gsumzadd.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
11 | | gsumzadd.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) |
12 | 1 | submss 17736 |
. . . 4
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ 𝐵) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
14 | 10, 13 | fssd 6305 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
15 | | gsumzadd.h |
. . 3
⊢ (𝜑 → 𝐻:𝐴⟶𝑆) |
16 | 15, 13 | fssd 6305 |
. 2
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
17 | | gsumzadd.c |
. . 3
⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑆)) |
18 | 10 | frnd 6298 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ 𝑆) |
19 | 4 | cntzidss 18153 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran 𝐹 ⊆ 𝑆) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
20 | 17, 18, 19 | syl2anc 579 |
. 2
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
21 | 15 | frnd 6298 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ 𝑆) |
22 | 4 | cntzidss 18153 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran 𝐻 ⊆ 𝑆) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
23 | 17, 21, 22 | syl2anc 579 |
. 2
⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
24 | 3 | submcl 17739 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
25 | 24 | 3expb 1110 |
. . . . . 6
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
26 | 11, 25 | sylan 575 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
27 | | inidm 4042 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
28 | 26, 10, 15, 6, 6, 27 | off 7189 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝑆) |
29 | 28 | frnd 6298 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ 𝑆) |
30 | 4 | cntzidss 18153 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran (𝐹 ∘𝑓 + 𝐻) ⊆ 𝑆) → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
31 | 17, 29, 30 | syl2anc 579 |
. 2
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
32 | 17 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ (𝑍‘𝑆)) |
33 | 13 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ 𝐵) |
34 | 5 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝐺 ∈ Mnd) |
35 | | vex 3400 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑥 ∈ V) |
37 | 11 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ∈ (SubMnd‘𝐺)) |
38 | | simpl 476 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥)) → 𝑥 ⊆ 𝐴) |
39 | | fssres 6320 |
. . . . . . . 8
⊢ ((𝐻:𝐴⟶𝑆 ∧ 𝑥 ⊆ 𝐴) → (𝐻 ↾ 𝑥):𝑥⟶𝑆) |
40 | 15, 38, 39 | syl2an 589 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 ↾ 𝑥):𝑥⟶𝑆) |
41 | 23 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
42 | | resss 5671 |
. . . . . . . . 9
⊢ (𝐻 ↾ 𝑥) ⊆ 𝐻 |
43 | | rnss 5599 |
. . . . . . . . 9
⊢ ((𝐻 ↾ 𝑥) ⊆ 𝐻 → ran (𝐻 ↾ 𝑥) ⊆ ran 𝐻) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(𝐻 ↾ 𝑥) ⊆ ran 𝐻 |
45 | 4 | cntzidss 18153 |
. . . . . . . 8
⊢ ((ran
𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ 𝑥) ⊆ ran 𝐻) → ran (𝐻 ↾ 𝑥) ⊆ (𝑍‘ran (𝐻 ↾ 𝑥))) |
46 | 41, 44, 45 | sylancl 580 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ran (𝐻 ↾ 𝑥) ⊆ (𝑍‘ran (𝐻 ↾ 𝑥))) |
47 | 15 | ffund 6295 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐻) |
48 | | funres 6177 |
. . . . . . . . . 10
⊢ (Fun
𝐻 → Fun (𝐻 ↾ 𝑥)) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun (𝐻 ↾ 𝑥)) |
50 | 49 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → Fun (𝐻 ↾ 𝑥)) |
51 | 8 | fsuppimpd 8570 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ∈
Fin) |
52 | 51 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 supp 0 ) ∈
Fin) |
53 | | fex 6761 |
. . . . . . . . . . . 12
⊢ ((𝐻:𝐴⟶𝑆 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
54 | 15, 6, 53 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ V) |
55 | 2 | fvexi 6460 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
56 | | ressuppss 7595 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ V ∧ 0 ∈ V)
→ ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
57 | 54, 55, 56 | sylancl 580 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
58 | 57 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
59 | | ssfi 8468 |
. . . . . . . . 9
⊢ (((𝐻 supp 0 ) ∈ Fin ∧ ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) → ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin) |
60 | 52, 58, 59 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin) |
61 | | resfunexg 6751 |
. . . . . . . . . . 11
⊢ ((Fun
𝐻 ∧ 𝑥 ∈ V) → (𝐻 ↾ 𝑥) ∈ V) |
62 | 47, 35, 61 | sylancl 580 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 ↾ 𝑥) ∈ V) |
63 | | isfsupp 8567 |
. . . . . . . . . 10
⊢ (((𝐻 ↾ 𝑥) ∈ V ∧ 0 ∈ V) → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
64 | 62, 55, 63 | sylancl 580 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
65 | 64 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
66 | 50, 60, 65 | mpbir2and 703 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 ↾ 𝑥) finSupp 0 ) |
67 | 2, 4, 34, 36, 37, 40, 46, 66 | gsumzsubmcl 18704 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐺 Σg (𝐻 ↾ 𝑥)) ∈ 𝑆) |
68 | 67 | snssd 4571 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ 𝑆) |
69 | 1, 4 | cntz2ss 18148 |
. . . . 5
⊢ ((𝑆 ⊆ 𝐵 ∧ {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
70 | 33, 68, 69 | syl2anc 579 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝑍‘𝑆) ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
71 | 32, 70 | sstrd 3830 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
72 | | eldifi 3954 |
. . . . 5
⊢ (𝑘 ∈ (𝐴 ∖ 𝑥) → 𝑘 ∈ 𝐴) |
73 | 72 | adantl 475 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥)) → 𝑘 ∈ 𝐴) |
74 | | ffvelrn 6621 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑆 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝑆) |
75 | 10, 73, 74 | syl2an 589 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ 𝑆) |
76 | 71, 75 | sseldd 3821 |
. 2
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
77 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 14,
16, 20, 23, 31, 76 | gsumzaddlem 18707 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |