Step | Hyp | Ref
| Expression |
1 | | gsumpt.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | | gsumpt.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
3 | 2 | snssd 4340 |
. . . 4
⊢ (𝜑 → {𝑋} ⊆ 𝐴) |
4 | 1, 3 | feqresmpt 6250 |
. . 3
⊢ (𝜑 → (𝐹 ↾ {𝑋}) = (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) |
5 | 4 | oveq2d 6666 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ {𝑋})) = (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎)))) |
6 | | gsumpt.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
7 | | gsumpt.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
8 | | eqid 2622 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
9 | | gsumpt.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
10 | | gsumpt.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
11 | 1, 2 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵) |
12 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))) |
13 | | eqid 2622 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
14 | 6, 13, 8 | elcntzsn 17758 |
. . . . . . . . 9
⊢ ((𝐹‘𝑋) ∈ 𝐵 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
15 | 11, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
16 | 11, 12, 15 | mpbir2and 957 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) |
17 | 16 | snssd 4340 |
. . . . . 6
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) |
18 | | eqid 2622 |
. . . . . . 7
⊢
(mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺)) |
19 | | eqid 2622 |
. . . . . . 7
⊢ (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) = (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
20 | 8, 18, 19 | cntzspan 18247 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ {(𝐹‘𝑋)} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
21 | 9, 17, 20 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
22 | 6 | submacs 17365 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
23 | | acsmre 16313 |
. . . . . . . 8
⊢
((SubMnd‘𝐺)
∈ (ACS‘𝐵) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
24 | 9, 22, 23 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (SubMnd‘𝐺) ∈ (Moore‘𝐵)) |
25 | 11 | snssd 4340 |
. . . . . . 7
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ 𝐵) |
26 | 18 | mrccl 16271 |
. . . . . . 7
⊢
(((SubMnd‘𝐺)
∈ (Moore‘𝐵)
∧ {(𝐹‘𝑋)} ⊆ 𝐵) → ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
27 | 24, 25, 26 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
28 | 19, 8 | submcmn2 18244 |
. . . . . 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 222 |
. . . 4
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
31 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
32 | 1, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) |
33 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → 𝑎 = 𝑋) |
34 | 33 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) = (𝐹‘𝑋)) |
35 | 24, 18, 25 | mrcssidd 16285 |
. . . . . . . . . . 11
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
36 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑋) ∈ V |
37 | 36 | snss 4316 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
38 | 35, 37 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
39 | 38 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
40 | 34, 39 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
41 | | eldifsn 4317 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝐴 ∖ {𝑋}) ↔ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) |
42 | | gsumpt.s |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ {𝑋}) |
43 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) ∈ V |
44 | 7, 43 | eqeltri 2697 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
45 | 44 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ V) |
46 | 1, 42, 10, 45 | suppssr 7326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 ∖ {𝑋})) → (𝐹‘𝑎) = 0 ) |
47 | 41, 46 | sylan2br 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) = 0 ) |
48 | 7 | subm0cl 17352 |
. . . . . . . . . . . 12
⊢
(((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
49 | 27, 48 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
50 | 49 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
51 | 47, 50 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
52 | 51 | anassrs 680 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 ≠ 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
53 | 40, 52 | pm2.61dane 2881 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
54 | 53 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
55 | | ffnfv 6388 |
. . . . . 6
⊢ (𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
56 | 32, 54, 55 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
57 | | frn 6053 |
. . . . 5
⊢ (𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
58 | 56, 57 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
59 | 8 | cntzidss 17770 |
. . . 4
⊢
((((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∧ ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
60 | 30, 58, 59 | syl2anc 693 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
61 | | ffun 6048 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
62 | 1, 61 | syl 17 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
63 | | snfi 8038 |
. . . . 5
⊢ {𝑋} ∈ Fin |
64 | | ssfi 8180 |
. . . . 5
⊢ (({𝑋} ∈ Fin ∧ (𝐹 supp 0 ) ⊆ {𝑋}) → (𝐹 supp 0 ) ∈
Fin) |
65 | 63, 42, 64 | sylancr 695 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
66 | | fex 6490 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
67 | 1, 10, 66 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ V) |
68 | | isfsupp 8279 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ (𝐹 finSupp 0 ↔ (Fun
𝐹 ∧ (𝐹 supp 0 ) ∈
Fin))) |
69 | 67, 45, 68 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐹 finSupp 0 ↔ (Fun 𝐹 ∧ (𝐹 supp 0 ) ∈
Fin))) |
70 | 62, 65, 69 | mpbir2and 957 |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
71 | 6, 7, 8, 9, 10, 1,
60, 42, 70 | gsumzres 18310 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ {𝑋})) = (𝐺 Σg 𝐹)) |
72 | | fveq2 6191 |
. . . 4
⊢ (𝑎 = 𝑋 → (𝐹‘𝑎) = (𝐹‘𝑋)) |
73 | 6, 72 | gsumsn 18354 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ 𝐵) → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
74 | 9, 2, 11, 73 | syl3anc 1326 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
75 | 5, 71, 74 | 3eqtr3d 2664 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐹‘𝑋)) |