Step |
Hyp |
Ref |
Expression |
1 |
|
gsumzsubmcl.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
2 |
|
gsumzsubmcl.z |
⊢ 𝑍 = ( Cntz ‘ 𝐺 ) |
3 |
|
gsumzsubmcl.g |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
4 |
|
gsumzsubmcl.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
5 |
|
gsumzsubmcl.s |
⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) |
6 |
|
gsumzsubmcl.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 ) |
7 |
|
gsumzsubmcl.c |
⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) |
8 |
|
gsumzsubmcl.w |
⊢ ( 𝜑 → 𝐹 finSupp 0 ) |
9 |
|
eqid |
⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) |
10 |
|
eqid |
⊢ ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) = ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) |
11 |
|
eqid |
⊢ ( Cntz ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Cntz ‘ ( 𝐺 ↾s 𝑆 ) ) |
12 |
|
eqid |
⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 ) |
13 |
12
|
submmnd |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) |
14 |
5 13
|
syl |
⊢ ( 𝜑 → ( 𝐺 ↾s 𝑆 ) ∈ Mnd ) |
15 |
12
|
submbas |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
16 |
5 15
|
syl |
⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
17 |
16
|
feq3d |
⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝑆 ↔ 𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) ) |
18 |
6 17
|
mpbid |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
19 |
6
|
frnd |
⊢ ( 𝜑 → ran 𝐹 ⊆ 𝑆 ) |
20 |
7 19
|
ssind |
⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( 𝑍 ‘ ran 𝐹 ) ∩ 𝑆 ) ) |
21 |
12 2 11
|
resscntz |
⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ran 𝐹 ⊆ 𝑆 ) → ( ( Cntz ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ ran 𝐹 ) = ( ( 𝑍 ‘ ran 𝐹 ) ∩ 𝑆 ) ) |
22 |
5 19 21
|
syl2anc |
⊢ ( 𝜑 → ( ( Cntz ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ ran 𝐹 ) = ( ( 𝑍 ‘ ran 𝐹 ) ∩ 𝑆 ) ) |
23 |
20 22
|
sseqtrrd |
⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ ran 𝐹 ) ) |
24 |
12 1
|
subm0 |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 0 = ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
25 |
5 24
|
syl |
⊢ ( 𝜑 → 0 = ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
26 |
8 25
|
breqtrd |
⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
27 |
9 10 11 14 4 18 23 26
|
gsumzcl |
⊢ ( 𝜑 → ( ( 𝐺 ↾s 𝑆 ) Σg 𝐹 ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
28 |
4 5 6 12
|
gsumsubm |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 ↾s 𝑆 ) Σg 𝐹 ) ) |
29 |
27 28 16
|
3eltr4d |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝑆 ) |