Step |
Hyp |
Ref |
Expression |
1 |
|
gsumzcl.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
gsumzcl.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
gsumzcl.z |
⊢ 𝑍 = ( Cntz ‘ 𝐺 ) |
4 |
|
gsumzcl.g |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
5 |
|
gsumzcl.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
6 |
|
gsumzcl.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
7 |
|
gsumzcl.c |
⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) |
8 |
|
gsumzcl.w |
⊢ ( 𝜑 → 𝐹 finSupp 0 ) |
9 |
|
gsumzf1o.h |
⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1-onto→ 𝐴 ) |
10 |
2
|
gsumz |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 ) |
11 |
4 5 10
|
syl2anc |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 ) |
12 |
|
f1of1 |
⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → 𝐻 : 𝐶 –1-1→ 𝐴 ) |
13 |
9 12
|
syl |
⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1→ 𝐴 ) |
14 |
|
f1dmex |
⊢ ( ( 𝐻 : 𝐶 –1-1→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐶 ∈ V ) |
15 |
13 5 14
|
syl2anc |
⊢ ( 𝜑 → 𝐶 ∈ V ) |
16 |
2
|
gsumz |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐶 ∈ V ) → ( 𝐺 Σg ( 𝑥 ∈ 𝐶 ↦ 0 ) ) = 0 ) |
17 |
4 15 16
|
syl2anc |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐶 ↦ 0 ) ) = 0 ) |
18 |
11 17
|
eqtr4d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐶 ↦ 0 ) ) ) |
19 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐶 ↦ 0 ) ) ) |
20 |
2
|
fvexi |
⊢ 0 ∈ V |
21 |
20
|
a1i |
⊢ ( 𝜑 → 0 ∈ V ) |
22 |
|
ssidd |
⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
23 |
6 5 21 22
|
gsumcllem |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 0 ) ) |
24 |
23
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) ) |
25 |
|
f1of |
⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → 𝐻 : 𝐶 ⟶ 𝐴 ) |
26 |
9 25
|
syl |
⊢ ( 𝜑 → 𝐻 : 𝐶 ⟶ 𝐴 ) |
27 |
26
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐻 : 𝐶 ⟶ 𝐴 ) |
28 |
27
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐴 ) |
29 |
27
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → 𝐻 = ( 𝑥 ∈ 𝐶 ↦ ( 𝐻 ‘ 𝑥 ) ) ) |
30 |
|
eqidd |
⊢ ( 𝑘 = ( 𝐻 ‘ 𝑥 ) → 0 = 0 ) |
31 |
28 29 23 30
|
fmptco |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐹 ∘ 𝐻 ) = ( 𝑥 ∈ 𝐶 ↦ 0 ) ) |
32 |
31
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐶 ↦ 0 ) ) ) |
33 |
19 24 32
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝐹 supp 0 ) = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) |
34 |
33
|
ex |
⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) ) |
35 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐻 : 𝐶 –1-1-onto→ 𝐴 ) |
36 |
|
f1ococnv2 |
⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → ( 𝐻 ∘ ◡ 𝐻 ) = ( I ↾ 𝐴 ) ) |
37 |
35 36
|
syl |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐻 ∘ ◡ 𝐻 ) = ( I ↾ 𝐴 ) ) |
38 |
37
|
coeq1d |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐻 ∘ ◡ 𝐻 ) ∘ 𝑓 ) = ( ( I ↾ 𝐴 ) ∘ 𝑓 ) ) |
39 |
|
f1of1 |
⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ) |
40 |
39
|
ad2antll |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ) |
41 |
|
suppssdm |
⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹 |
42 |
41 6
|
fssdm |
⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 ) |
43 |
42
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 ) |
44 |
|
f1ss |
⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ ( 𝐹 supp 0 ) ∧ ( 𝐹 supp 0 ) ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 ) |
45 |
40 43 44
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 ) |
46 |
|
f1f |
⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 ) |
47 |
|
fcoi2 |
⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 ) |
48 |
45 46 47
|
3syl |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 ) |
49 |
38 48
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐻 ∘ ◡ 𝐻 ) ∘ 𝑓 ) = 𝑓 ) |
50 |
|
coass |
⊢ ( ( 𝐻 ∘ ◡ 𝐻 ) ∘ 𝑓 ) = ( 𝐻 ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) |
51 |
49 50
|
eqtr3di |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝑓 = ( 𝐻 ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) |
52 |
51
|
coeq2d |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ ( 𝐻 ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) ) |
53 |
|
coass |
⊢ ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) = ( 𝐹 ∘ ( 𝐻 ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) |
54 |
52 53
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ∘ 𝑓 ) = ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) |
55 |
54
|
seqeq3d |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) ) |
56 |
55
|
fveq1d |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) |
57 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
58 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐺 ∈ Mnd ) |
59 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐴 ∈ 𝑉 ) |
60 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
61 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) |
62 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) |
63 |
|
ssid |
⊢ ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) |
64 |
|
f1ofo |
⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) ) |
65 |
|
forn |
⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) ) |
66 |
64 65
|
syl |
⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ran 𝑓 = ( 𝐹 supp 0 ) ) |
67 |
66
|
ad2antll |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran 𝑓 = ( 𝐹 supp 0 ) ) |
68 |
63 67
|
sseqtrrid |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 ) |
69 |
|
eqid |
⊢ ( ( 𝐹 ∘ 𝑓 ) supp 0 ) = ( ( 𝐹 ∘ 𝑓 ) supp 0 ) |
70 |
1 2 57 3 58 59 60 61 62 45 68 69
|
gsumval3 |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) |
71 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → 𝐶 ∈ V ) |
72 |
|
fco |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐻 : 𝐶 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 ) |
73 |
6 26 72
|
syl2anc |
⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 ) |
74 |
73
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 ) |
75 |
|
rncoss |
⊢ ran ( 𝐹 ∘ 𝐻 ) ⊆ ran 𝐹 |
76 |
3
|
cntzidss |
⊢ ( ( ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ∧ ran ( 𝐹 ∘ 𝐻 ) ⊆ ran 𝐹 ) → ran ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘ 𝐻 ) ) ) |
77 |
7 75 76
|
sylancl |
⊢ ( 𝜑 → ran ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘ 𝐻 ) ) ) |
78 |
77
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ran ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘ 𝐻 ) ) ) |
79 |
|
f1ocnv |
⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐻 : 𝐴 –1-1-onto→ 𝐶 ) |
80 |
|
f1of1 |
⊢ ( ◡ 𝐻 : 𝐴 –1-1-onto→ 𝐶 → ◡ 𝐻 : 𝐴 –1-1→ 𝐶 ) |
81 |
9 79 80
|
3syl |
⊢ ( 𝜑 → ◡ 𝐻 : 𝐴 –1-1→ 𝐶 ) |
82 |
81
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ◡ 𝐻 : 𝐴 –1-1→ 𝐶 ) |
83 |
|
f1co |
⊢ ( ( ◡ 𝐻 : 𝐴 –1-1→ 𝐶 ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐴 ) → ( ◡ 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐶 ) |
84 |
82 45 83
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1→ 𝐶 ) |
85 |
|
ssidd |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
86 |
6 5
|
fexd |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
87 |
|
suppimacnv |
⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) |
88 |
86 20 87
|
sylancl |
⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) |
89 |
88
|
eqcomd |
⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 supp 0 ) ) |
90 |
89
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ( 𝐹 supp 0 ) ) |
91 |
85 90 67
|
3sstr4d |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ran 𝑓 ) |
92 |
|
imass2 |
⊢ ( ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ⊆ ran 𝑓 → ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ⊆ ( ◡ 𝐻 “ ran 𝑓 ) ) |
93 |
91 92
|
syl |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) ⊆ ( ◡ 𝐻 “ ran 𝑓 ) ) |
94 |
|
cnvco |
⊢ ◡ ( 𝐹 ∘ 𝐻 ) = ( ◡ 𝐻 ∘ ◡ 𝐹 ) |
95 |
94
|
imaeq1i |
⊢ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) = ( ( ◡ 𝐻 ∘ ◡ 𝐹 ) “ ( V ∖ { 0 } ) ) |
96 |
|
imaco |
⊢ ( ( ◡ 𝐻 ∘ ◡ 𝐹 ) “ ( V ∖ { 0 } ) ) = ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) |
97 |
95 96
|
eqtri |
⊢ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) = ( ◡ 𝐻 “ ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) ) |
98 |
|
rnco2 |
⊢ ran ( ◡ 𝐻 ∘ 𝑓 ) = ( ◡ 𝐻 “ ran 𝑓 ) |
99 |
93 97 98
|
3sstr4g |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ) |
100 |
|
f1oexrnex |
⊢ ( ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 ∈ V ) |
101 |
9 5 100
|
syl2anc |
⊢ ( 𝜑 → 𝐻 ∈ V ) |
102 |
|
coexg |
⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐹 ∘ 𝐻 ) ∈ V ) |
103 |
86 101 102
|
syl2anc |
⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ V ) |
104 |
|
suppimacnv |
⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ) |
105 |
103 20 104
|
sylancl |
⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ) |
106 |
105
|
sseq1d |
⊢ ( 𝜑 → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ↔ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ) ) |
107 |
106
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ↔ ( ◡ ( 𝐹 ∘ 𝐻 ) “ ( V ∖ { 0 } ) ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ) ) |
108 |
99 107
|
mpbird |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ ran ( ◡ 𝐻 ∘ 𝑓 ) ) |
109 |
|
eqid |
⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) supp 0 ) = ( ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) supp 0 ) |
110 |
1 2 57 3 58 71 74 78 62 84 108 109
|
gsumval3 |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ( 𝐹 ∘ 𝐻 ) ∘ ( ◡ 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) |
111 |
56 70 110
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) |
112 |
111
|
expr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) ) |
113 |
112
|
exlimdv |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) ) |
114 |
113
|
expimpd |
⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) ) |
115 |
|
fsuppimp |
⊢ ( 𝐹 finSupp 0 → ( Fun 𝐹 ∧ ( 𝐹 supp 0 ) ∈ Fin ) ) |
116 |
115
|
simprd |
⊢ ( 𝐹 finSupp 0 → ( 𝐹 supp 0 ) ∈ Fin ) |
117 |
|
fz1f1o |
⊢ ( ( 𝐹 supp 0 ) ∈ Fin → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) ) |
118 |
8 116 117
|
3syl |
⊢ ( 𝜑 → ( ( 𝐹 supp 0 ) = ∅ ∨ ( ( ♯ ‘ ( 𝐹 supp 0 ) ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) ) ) |
119 |
34 114 118
|
mpjaod |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) ) |