Step | Hyp | Ref
| Expression |
1 | | gsumpt.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | | gsumpt.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
3 | 2 | snssd 4742 |
. . . 4
⊢ (𝜑 → {𝑋} ⊆ 𝐴) |
4 | 1, 3 | feqresmpt 6838 |
. . 3
⊢ (𝜑 → (𝐹 ↾ {𝑋}) = (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) |
5 | 4 | oveq2d 7291 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ {𝑋})) = (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎)))) |
6 | | gsumpt.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
7 | | gsumpt.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
8 | | eqid 2738 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
9 | | gsumpt.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
10 | | gsumpt.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
11 | 1, 2 | ffvelrnd 6962 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵) |
12 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))) |
13 | | eqid 2738 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
14 | 6, 13, 8 | elcntzsn 18931 |
. . . . . . . . 9
⊢ ((𝐹‘𝑋) ∈ 𝐵 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
15 | 11, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
16 | 11, 12, 15 | mpbir2and 710 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) |
17 | 16 | snssd 4742 |
. . . . . 6
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) |
18 | | eqid 2738 |
. . . . . . 7
⊢
(mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺)) |
19 | | eqid 2738 |
. . . . . . 7
⊢ (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) = (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
20 | 8, 18, 19 | cntzspan 19445 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ {(𝐹‘𝑋)} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
21 | 9, 17, 20 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
22 | 6 | submacs 18465 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
23 | | acsmre 17361 |
. . . . . . . 8
⊢
((SubMnd‘𝐺)
∈ (ACS‘𝐵) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
24 | 9, 22, 23 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (SubMnd‘𝐺) ∈ (Moore‘𝐵)) |
25 | 11 | snssd 4742 |
. . . . . . 7
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ 𝐵) |
26 | 18 | mrccl 17320 |
. . . . . . 7
⊢
(((SubMnd‘𝐺)
∈ (Moore‘𝐵)
∧ {(𝐹‘𝑋)} ⊆ 𝐵) → ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
27 | 24, 25, 26 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
28 | 19, 8 | submcmn2 19440 |
. . . . . 6
⊢
(((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺) → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})))) |
29 | 27, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})))) |
30 | 21, 29 | mpbid 231 |
. . . 4
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
31 | 1 | ffnd 6601 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) |
32 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → 𝑎 = 𝑋) |
33 | 32 | fveq2d 6778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) = (𝐹‘𝑋)) |
34 | 24, 18, 25 | mrcssidd 17334 |
. . . . . . . . . . 11
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
35 | | fvex 6787 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑋) ∈ V |
36 | 35 | snss 4719 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
37 | 34, 36 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
38 | 37 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
39 | 33, 38 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
40 | | eldifsn 4720 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝐴 ∖ {𝑋}) ↔ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) |
41 | | gsumpt.s |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ {𝑋}) |
42 | 7 | fvexi 6788 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ V) |
44 | 1, 41, 10, 43 | suppssr 8012 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 ∖ {𝑋})) → (𝐹‘𝑎) = 0 ) |
45 | 40, 44 | sylan2br 595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) = 0 ) |
46 | 7 | subm0cl 18450 |
. . . . . . . . . . . 12
⊢
(((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
47 | 27, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
48 | 47 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
49 | 45, 48 | eqeltrd 2839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
50 | 49 | anassrs 468 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 ≠ 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
51 | 39, 50 | pm2.61dane 3032 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
52 | 51 | ralrimiva 3103 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
53 | | ffnfv 6992 |
. . . . . 6
⊢ (𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
54 | 31, 52, 53 | sylanbrc 583 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
55 | 54 | frnd 6608 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
56 | 8 | cntzidss 18944 |
. . . 4
⊢
((((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∧ ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
57 | 30, 55, 56 | syl2anc 584 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
58 | 1 | ffund 6604 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
59 | | snfi 8834 |
. . . . 5
⊢ {𝑋} ∈ Fin |
60 | | ssfi 8956 |
. . . . 5
⊢ (({𝑋} ∈ Fin ∧ (𝐹 supp 0 ) ⊆ {𝑋}) → (𝐹 supp 0 ) ∈
Fin) |
61 | 59, 41, 60 | sylancr 587 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
62 | 1, 10 | fexd 7103 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ V) |
63 | | isfsupp 9132 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ (𝐹 finSupp 0 ↔ (Fun
𝐹 ∧ (𝐹 supp 0 ) ∈
Fin))) |
64 | 62, 43, 63 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐹 finSupp 0 ↔ (Fun 𝐹 ∧ (𝐹 supp 0 ) ∈
Fin))) |
65 | 58, 61, 64 | mpbir2and 710 |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
66 | 6, 7, 8, 9, 10, 1,
57, 41, 65 | gsumzres 19510 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ {𝑋})) = (𝐺 Σg 𝐹)) |
67 | | fveq2 6774 |
. . . 4
⊢ (𝑎 = 𝑋 → (𝐹‘𝑎) = (𝐹‘𝑋)) |
68 | 6, 67 | gsumsn 19555 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ 𝐵) → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
69 | 9, 2, 11, 68 | syl3anc 1370 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
70 | 5, 66, 69 | 3eqtr3d 2786 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐹‘𝑋)) |