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 2610 |
. 2
⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐹 ∪ 𝐻) supp 0 ) |
10 | | gsumzadd.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
11 | | gsumzadd.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) |
12 | 1 | submss 17173 |
. . . 4
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ 𝐵) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
14 | 10, 13 | fssd 5970 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
15 | | gsumzadd.h |
. . 3
⊢ (𝜑 → 𝐻:𝐴⟶𝑆) |
16 | 15, 13 | fssd 5970 |
. 2
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
17 | | gsumzadd.c |
. . 3
⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑆)) |
18 | | frn 5966 |
. . . 4
⊢ (𝐹:𝐴⟶𝑆 → ran 𝐹 ⊆ 𝑆) |
19 | 10, 18 | syl 17 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ 𝑆) |
20 | 4 | cntzidss 17593 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran 𝐹 ⊆ 𝑆) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
21 | 17, 19, 20 | syl2anc 691 |
. 2
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
22 | | frn 5966 |
. . . 4
⊢ (𝐻:𝐴⟶𝑆 → ran 𝐻 ⊆ 𝑆) |
23 | 15, 22 | syl 17 |
. . 3
⊢ (𝜑 → ran 𝐻 ⊆ 𝑆) |
24 | 4 | cntzidss 17593 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran 𝐻 ⊆ 𝑆) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
25 | 17, 23, 24 | syl2anc 691 |
. 2
⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
26 | 3 | submcl 17176 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
27 | 26 | 3expb 1258 |
. . . . . 6
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
28 | 11, 27 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
29 | | inidm 3784 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
30 | 28, 10, 15, 6, 6, 29 | off 6810 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝑆) |
31 | | frn 5966 |
. . . 4
⊢ ((𝐹 ∘𝑓
+ 𝐻):𝐴⟶𝑆 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ 𝑆) |
32 | 30, 31 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ 𝑆) |
33 | 4 | cntzidss 17593 |
. . 3
⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ ran (𝐹 ∘𝑓 + 𝐻) ⊆ 𝑆) → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
34 | 17, 32, 33 | syl2anc 691 |
. 2
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) |
35 | 17 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ (𝑍‘𝑆)) |
36 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ 𝐵) |
37 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝐺 ∈ Mnd) |
38 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑥 ∈ V) |
40 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ∈ (SubMnd‘𝐺)) |
41 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥)) → 𝑥 ⊆ 𝐴) |
42 | | fssres 5983 |
. . . . . . . 8
⊢ ((𝐻:𝐴⟶𝑆 ∧ 𝑥 ⊆ 𝐴) → (𝐻 ↾ 𝑥):𝑥⟶𝑆) |
43 | 15, 41, 42 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 ↾ 𝑥):𝑥⟶𝑆) |
44 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) |
45 | | resss 5342 |
. . . . . . . . 9
⊢ (𝐻 ↾ 𝑥) ⊆ 𝐻 |
46 | | rnss 5275 |
. . . . . . . . 9
⊢ ((𝐻 ↾ 𝑥) ⊆ 𝐻 → ran (𝐻 ↾ 𝑥) ⊆ ran 𝐻) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(𝐻 ↾ 𝑥) ⊆ ran 𝐻 |
48 | 4 | cntzidss 17593 |
. . . . . . . 8
⊢ ((ran
𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ 𝑥) ⊆ ran 𝐻) → ran (𝐻 ↾ 𝑥) ⊆ (𝑍‘ran (𝐻 ↾ 𝑥))) |
49 | 44, 47, 48 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ran (𝐻 ↾ 𝑥) ⊆ (𝑍‘ran (𝐻 ↾ 𝑥))) |
50 | | ffun 5961 |
. . . . . . . . . . 11
⊢ (𝐻:𝐴⟶𝑆 → Fun 𝐻) |
51 | 15, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐻) |
52 | | funres 5843 |
. . . . . . . . . 10
⊢ (Fun
𝐻 → Fun (𝐻 ↾ 𝑥)) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun (𝐻 ↾ 𝑥)) |
54 | 53 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → Fun (𝐻 ↾ 𝑥)) |
55 | 8 | fsuppimpd 8165 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 supp 0 ) ∈
Fin) |
56 | 55 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 supp 0 ) ∈
Fin) |
57 | | fex 6394 |
. . . . . . . . . . . 12
⊢ ((𝐻:𝐴⟶𝑆 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
58 | 15, 6, 57 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ V) |
59 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(0g‘𝐺) ∈ V |
60 | 2, 59 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
61 | | ressuppss 7201 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ V ∧ 0 ∈ V)
→ ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
62 | 58, 60, 61 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
63 | 62 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) |
64 | | ssfi 8065 |
. . . . . . . . 9
⊢ (((𝐻 supp 0 ) ∈ Fin ∧ ((𝐻 ↾ 𝑥) supp 0 ) ⊆ (𝐻 supp 0 )) → ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin) |
65 | 56, 63, 64 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin) |
66 | | resfunexg 6384 |
. . . . . . . . . . 11
⊢ ((Fun
𝐻 ∧ 𝑥 ∈ V) → (𝐻 ↾ 𝑥) ∈ V) |
67 | 51, 38, 66 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐻 ↾ 𝑥) ∈ V) |
68 | | isfsupp 8162 |
. . . . . . . . . 10
⊢ (((𝐻 ↾ 𝑥) ∈ V ∧ 0 ∈ V) → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
69 | 67, 60, 68 | sylancl 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
70 | 69 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → ((𝐻 ↾ 𝑥) finSupp 0 ↔ (Fun (𝐻 ↾ 𝑥) ∧ ((𝐻 ↾ 𝑥) supp 0 ) ∈
Fin))) |
71 | 54, 65, 70 | mpbir2and 959 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐻 ↾ 𝑥) finSupp 0 ) |
72 | 2, 4, 37, 39, 40, 43, 49, 71 | gsumzsubmcl 18141 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐺 Σg (𝐻 ↾ 𝑥)) ∈ 𝑆) |
73 | 72 | snssd 4281 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ 𝑆) |
74 | 1, 4 | cntz2ss 17588 |
. . . . 5
⊢ ((𝑆 ⊆ 𝐵 ∧ {(𝐺 Σg (𝐻 ↾ 𝑥))} ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
75 | 36, 73, 74 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝑍‘𝑆) ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
76 | 35, 75 | sstrd 3578 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → 𝑆 ⊆ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
77 | | eldifi 3694 |
. . . . 5
⊢ (𝑘 ∈ (𝐴 ∖ 𝑥) → 𝑘 ∈ 𝐴) |
78 | 77 | adantl 481 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥)) → 𝑘 ∈ 𝐴) |
79 | | ffvelrn 6265 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑆 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝑆) |
80 | 10, 78, 79 | syl2an 493 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ 𝑆) |
81 | 76, 80 | sseldd 3569 |
. 2
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) |
82 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 14,
16, 21, 25, 34, 81 | gsumzaddlem 18144 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓
+ 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |