Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsmhm.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
tsmsmhm.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
3 |
|
tsmsmhm.k |
⊢ 𝐾 = ( TopOpen ‘ 𝐻 ) |
4 |
|
tsmsmhm.1 |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
5 |
|
tsmsmhm.2 |
⊢ ( 𝜑 → 𝐺 ∈ TopSp ) |
6 |
|
tsmsmhm.3 |
⊢ ( 𝜑 → 𝐻 ∈ CMnd ) |
7 |
|
tsmsmhm.4 |
⊢ ( 𝜑 → 𝐻 ∈ TopSp ) |
8 |
|
tsmsmhm.5 |
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 MndHom 𝐻 ) ) |
9 |
|
tsmsmhm.6 |
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐽 Cn 𝐾 ) ) |
10 |
|
tsmsmhm.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
11 |
|
tsmsmhm.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
12 |
|
tsmsmhm.x |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) ) |
13 |
1 2
|
istps |
⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐵 ) ) |
14 |
5 13
|
sylib |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) ) |
15 |
|
eqid |
⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin ) |
16 |
|
eqid |
⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) |
17 |
|
eqid |
⊢ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) = ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) |
18 |
15 16 17 10
|
tsmsfbas |
⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) ) |
19 |
|
fgcl |
⊢ ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) ) |
20 |
18 19
|
syl |
⊢ ( 𝜑 → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) ) |
21 |
1 15 4 10 11
|
tsmslem1 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝐵 ) |
22 |
21
|
fmpttd |
⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ 𝐵 ) |
23 |
1 2 15 17 5 10 11
|
tsmsval |
⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) |
24 |
12 23
|
eleqtrd |
⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) |
25 |
1 4 5 10 11
|
tsmscl |
⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 ) |
26 |
25 12
|
sseldd |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
27 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 ) |
28 |
14 27
|
syl |
⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 ) |
29 |
26 28
|
eleqtrd |
⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝐽 ) |
30 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
31 |
30
|
cncnpi |
⊢ ( ( 𝐶 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑋 ∈ ∪ 𝐽 ) → 𝐶 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑋 ) ) |
32 |
9 29 31
|
syl2anc |
⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑋 ) ) |
33 |
|
flfcnp |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ 𝐵 ) ∧ ( 𝑋 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ∧ 𝐶 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑋 ) ) ) → ( 𝐶 ‘ 𝑋 ) ∈ ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) ) |
34 |
14 20 22 24 32 33
|
syl32anc |
⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) ∈ ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) ) |
35 |
|
eqid |
⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 ) |
36 |
35 3
|
istps |
⊢ ( 𝐻 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ) |
37 |
7 36
|
sylib |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ) |
38 |
|
cnf2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ∧ 𝐶 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐶 : 𝐵 ⟶ ( Base ‘ 𝐻 ) ) |
39 |
14 37 9 38
|
syl3anc |
⊢ ( 𝜑 → 𝐶 : 𝐵 ⟶ ( Base ‘ 𝐻 ) ) |
40 |
|
fco |
⊢ ( ( 𝐶 : 𝐵 ⟶ ( Base ‘ 𝐻 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐶 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝐻 ) ) |
41 |
39 11 40
|
syl2anc |
⊢ ( 𝜑 → ( 𝐶 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝐻 ) ) |
42 |
35 3 15 17 6 10 41
|
tsmsval |
⊢ ( 𝜑 → ( 𝐻 tsums ( 𝐶 ∘ 𝐹 ) ) = ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶 ∘ 𝐹 ) ↾ 𝑧 ) ) ) ) ) |
43 |
39 21
|
cofmpt |
⊢ ( 𝜑 → ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) |
44 |
|
resco |
⊢ ( ( 𝐶 ∘ 𝐹 ) ↾ 𝑧 ) = ( 𝐶 ∘ ( 𝐹 ↾ 𝑧 ) ) |
45 |
44
|
oveq2i |
⊢ ( 𝐻 Σg ( ( 𝐶 ∘ 𝐹 ) ↾ 𝑧 ) ) = ( 𝐻 Σg ( 𝐶 ∘ ( 𝐹 ↾ 𝑧 ) ) ) |
46 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
47 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd ) |
48 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐻 ∈ CMnd ) |
49 |
|
cmnmnd |
⊢ ( 𝐻 ∈ CMnd → 𝐻 ∈ Mnd ) |
50 |
48 49
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐻 ∈ Mnd ) |
51 |
|
elinel2 |
⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin ) |
52 |
51
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin ) |
53 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐶 ∈ ( 𝐺 MndHom 𝐻 ) ) |
54 |
|
elfpw |
⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin ) ) |
55 |
54
|
simplbi |
⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ⊆ 𝐴 ) |
56 |
|
fssres |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 ) |
57 |
11 55 56
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 ) |
58 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 0g ‘ 𝐺 ) ∈ V ) |
59 |
57 52 58
|
fdmfifsupp |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) finSupp ( 0g ‘ 𝐺 ) ) |
60 |
1 46 47 50 52 53 57 59
|
gsummhm |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 Σg ( 𝐶 ∘ ( 𝐹 ↾ 𝑧 ) ) ) = ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) |
61 |
45 60
|
eqtrid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 Σg ( ( 𝐶 ∘ 𝐹 ) ↾ 𝑧 ) ) = ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) |
62 |
61
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶 ∘ 𝐹 ) ↾ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) |
63 |
43 62
|
eqtr4d |
⊢ ( 𝜑 → ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶 ∘ 𝐹 ) ↾ 𝑧 ) ) ) ) |
64 |
63
|
fveq2d |
⊢ ( 𝜑 → ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) = ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶 ∘ 𝐹 ) ↾ 𝑧 ) ) ) ) ) |
65 |
42 64
|
eqtr4d |
⊢ ( 𝜑 → ( 𝐻 tsums ( 𝐶 ∘ 𝐹 ) ) = ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) ) ) |
66 |
34 65
|
eleqtrrd |
⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) ∈ ( 𝐻 tsums ( 𝐶 ∘ 𝐹 ) ) ) |