Step |
Hyp |
Ref |
Expression |
1 |
|
gsumzadd.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
gsumzadd.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
gsumzadd.p |
⊢ + = ( +g ‘ 𝐺 ) |
4 |
|
gsumzadd.z |
⊢ 𝑍 = ( Cntz ‘ 𝐺 ) |
5 |
|
gsumzadd.g |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
6 |
|
gsumzadd.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
7 |
|
gsumzadd.fn |
⊢ ( 𝜑 → 𝐹 finSupp 0 ) |
8 |
|
gsumzadd.hn |
⊢ ( 𝜑 → 𝐻 finSupp 0 ) |
9 |
|
gsumzadd.s |
⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) |
10 |
|
gsumzadd.c |
⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) |
11 |
|
gsumzadd.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 ) |
12 |
|
gsumzadd.h |
⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝑆 ) |
13 |
|
eqid |
⊢ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) = ( ( 𝐹 ∪ 𝐻 ) supp 0 ) |
14 |
1
|
submss |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 ) |
15 |
9 14
|
syl |
⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 ) |
16 |
11 15
|
fssd |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
17 |
12 15
|
fssd |
⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 ) |
18 |
11
|
frnd |
⊢ ( 𝜑 → ran 𝐹 ⊆ 𝑆 ) |
19 |
4
|
cntzidss |
⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ ran 𝐹 ⊆ 𝑆 ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) |
20 |
10 18 19
|
syl2anc |
⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) |
21 |
12
|
frnd |
⊢ ( 𝜑 → ran 𝐻 ⊆ 𝑆 ) |
22 |
4
|
cntzidss |
⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ ran 𝐻 ⊆ 𝑆 ) → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) ) |
23 |
10 21 22
|
syl2anc |
⊢ ( 𝜑 → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) ) |
24 |
3
|
submcl |
⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 ) |
25 |
24
|
3expb |
⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 ) |
26 |
9 25
|
sylan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 ) |
27 |
|
inidm |
⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
28 |
26 11 12 6 6 27
|
off |
⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐻 ) : 𝐴 ⟶ 𝑆 ) |
29 |
28
|
frnd |
⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐻 ) ⊆ 𝑆 ) |
30 |
4
|
cntzidss |
⊢ ( ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ ran ( 𝐹 ∘f + 𝐻 ) ⊆ 𝑆 ) → ran ( 𝐹 ∘f + 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘f + 𝐻 ) ) ) |
31 |
10 29 30
|
syl2anc |
⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘f + 𝐻 ) ) ) |
32 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) |
33 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → 𝑆 ⊆ 𝐵 ) |
34 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → 𝐺 ∈ Mnd ) |
35 |
|
vex |
⊢ 𝑥 ∈ V |
36 |
35
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → 𝑥 ∈ V ) |
37 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) |
38 |
|
simpl |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) → 𝑥 ⊆ 𝐴 ) |
39 |
|
fssres |
⊢ ( ( 𝐻 : 𝐴 ⟶ 𝑆 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ 𝑆 ) |
40 |
12 38 39
|
syl2an |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ 𝑆 ) |
41 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) ) |
42 |
|
resss |
⊢ ( 𝐻 ↾ 𝑥 ) ⊆ 𝐻 |
43 |
42
|
rnssi |
⊢ ran ( 𝐻 ↾ 𝑥 ) ⊆ ran 𝐻 |
44 |
4
|
cntzidss |
⊢ ( ( ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) ∧ ran ( 𝐻 ↾ 𝑥 ) ⊆ ran 𝐻 ) → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( 𝑍 ‘ ran ( 𝐻 ↾ 𝑥 ) ) ) |
45 |
41 43 44
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ran ( 𝐻 ↾ 𝑥 ) ⊆ ( 𝑍 ‘ ran ( 𝐻 ↾ 𝑥 ) ) ) |
46 |
12
|
ffund |
⊢ ( 𝜑 → Fun 𝐻 ) |
47 |
46
|
funresd |
⊢ ( 𝜑 → Fun ( 𝐻 ↾ 𝑥 ) ) |
48 |
47
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → Fun ( 𝐻 ↾ 𝑥 ) ) |
49 |
8
|
fsuppimpd |
⊢ ( 𝜑 → ( 𝐻 supp 0 ) ∈ Fin ) |
50 |
49
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐻 supp 0 ) ∈ Fin ) |
51 |
12 6
|
fexd |
⊢ ( 𝜑 → 𝐻 ∈ V ) |
52 |
2
|
fvexi |
⊢ 0 ∈ V |
53 |
|
ressuppss |
⊢ ( ( 𝐻 ∈ V ∧ 0 ∈ V ) → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) ) |
54 |
51 52 53
|
sylancl |
⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) ) |
55 |
54
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) ) |
56 |
50 55
|
ssfid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin ) |
57 |
|
resfunexg |
⊢ ( ( Fun 𝐻 ∧ 𝑥 ∈ V ) → ( 𝐻 ↾ 𝑥 ) ∈ V ) |
58 |
46 35 57
|
sylancl |
⊢ ( 𝜑 → ( 𝐻 ↾ 𝑥 ) ∈ V ) |
59 |
|
isfsupp |
⊢ ( ( ( 𝐻 ↾ 𝑥 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐻 ↾ 𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻 ↾ 𝑥 ) ∧ ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin ) ) ) |
60 |
58 52 59
|
sylancl |
⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻 ↾ 𝑥 ) ∧ ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin ) ) ) |
61 |
60
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( ( 𝐻 ↾ 𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻 ↾ 𝑥 ) ∧ ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin ) ) ) |
62 |
48 56 61
|
mpbir2and |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) finSupp 0 ) |
63 |
2 4 34 36 37 40 45 62
|
gsumzsubmcl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) ∈ 𝑆 ) |
64 |
63
|
snssd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ 𝑆 ) |
65 |
1 4
|
cntz2ss |
⊢ ( ( 𝑆 ⊆ 𝐵 ∧ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) |
66 |
33 64 65
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) |
67 |
32 66
|
sstrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → 𝑆 ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) |
68 |
|
eldifi |
⊢ ( 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) → 𝑘 ∈ 𝐴 ) |
69 |
68
|
adantl |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) → 𝑘 ∈ 𝐴 ) |
70 |
|
ffvelrn |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑆 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) |
71 |
11 69 70
|
syl2an |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) |
72 |
67 71
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) |
73 |
1 2 3 4 5 6 7 8 13 16 17 20 23 31 72
|
gsumzaddlem |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) |