Step | Hyp | Ref
| Expression |
1 | | gsumpt.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | | gsumpt.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
3 | 2 | snssd 4694 |
. . . 4
⊢ (𝜑 → {𝑋} ⊆ 𝐴) |
4 | 1, 3 | feqresmpt 6732 |
. . 3
⊢ (𝜑 → (𝐹 ↾ {𝑋}) = (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) |
5 | 4 | oveq2d 7180 |
. 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 6856 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵) |
12 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))) |
13 | | eqid 2738 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
14 | 6, 13, 8 | elcntzsn 18566 |
. . . . . . . . 9
⊢ ((𝐹‘𝑋) ∈ 𝐵 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
15 | 11, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
16 | 11, 12, 15 | mpbir2and 713 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) |
17 | 16 | snssd 4694 |
. . . . . 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 19076 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ {(𝐹‘𝑋)} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
21 | 9, 17, 20 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
22 | 6 | submacs 18100 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
23 | | acsmre 17019 |
. . . . . . . 8
⊢
((SubMnd‘𝐺)
∈ (ACS‘𝐵) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
24 | 9, 22, 23 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (SubMnd‘𝐺) ∈ (Moore‘𝐵)) |
25 | 11 | snssd 4694 |
. . . . . . 7
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ 𝐵) |
26 | 18 | mrccl 16978 |
. . . . . . 7
⊢
(((SubMnd‘𝐺)
∈ (Moore‘𝐵)
∧ {(𝐹‘𝑋)} ⊆ 𝐵) → ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
27 | 24, 25, 26 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
28 | 19, 8 | submcmn2 19071 |
. . . . . 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 235 |
. . . 4
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
31 | 1 | ffnd 6499 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) |
32 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → 𝑎 = 𝑋) |
33 | 32 | fveq2d 6672 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) = (𝐹‘𝑋)) |
34 | 24, 18, 25 | mrcssidd 16992 |
. . . . . . . . . . 11
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
35 | | fvex 6681 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑋) ∈ V |
36 | 35 | snss 4671 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
37 | 34, 36 | sylibr 237 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
38 | 37 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
39 | 33, 38 | eqeltrd 2833 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
40 | | eldifsn 4672 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝐴 ∖ {𝑋}) ↔ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) |
41 | | gsumpt.s |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ {𝑋}) |
42 | 7 | fvexi 6682 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ V) |
44 | 1, 41, 10, 43 | suppssr 7884 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 ∖ {𝑋})) → (𝐹‘𝑎) = 0 ) |
45 | 40, 44 | sylan2br 598 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) = 0 ) |
46 | 7 | subm0cl 18085 |
. . . . . . . . . . . 12
⊢
(((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
47 | 27, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
48 | 47 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
49 | 45, 48 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
50 | 49 | anassrs 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 ≠ 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
51 | 39, 50 | pm2.61dane 3021 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
52 | 51 | ralrimiva 3096 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
53 | | ffnfv 6886 |
. . . . . 6
⊢ (𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
54 | 31, 52, 53 | sylanbrc 586 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
55 | 54 | frnd 6506 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
56 | 8 | cntzidss 18579 |
. . . 4
⊢
((((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∧ ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
57 | 30, 55, 56 | syl2anc 587 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ((Cntz‘𝐺)‘ran 𝐹)) |
58 | 1 | ffund 6502 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
59 | | snfi 8635 |
. . . . 5
⊢ {𝑋} ∈ Fin |
60 | | ssfi 8765 |
. . . . 5
⊢ (({𝑋} ∈ Fin ∧ (𝐹 supp 0 ) ⊆ {𝑋}) → (𝐹 supp 0 ) ∈
Fin) |
61 | 59, 41, 60 | sylancr 590 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
62 | 1, 10 | fexd 6994 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ V) |
63 | | isfsupp 8903 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ (𝐹 finSupp 0 ↔ (Fun
𝐹 ∧ (𝐹 supp 0 ) ∈
Fin))) |
64 | 62, 43, 63 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐹 finSupp 0 ↔ (Fun 𝐹 ∧ (𝐹 supp 0 ) ∈
Fin))) |
65 | 58, 61, 64 | mpbir2and 713 |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
66 | 6, 7, 8, 9, 10, 1,
57, 41, 65 | gsumzres 19141 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ {𝑋})) = (𝐺 Σg 𝐹)) |
67 | | fveq2 6668 |
. . . 4
⊢ (𝑎 = 𝑋 → (𝐹‘𝑎) = (𝐹‘𝑋)) |
68 | 6, 67 | gsumsn 19186 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ 𝐵) → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
69 | 9, 2, 11, 68 | syl3anc 1372 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
70 | 5, 66, 69 | 3eqtr3d 2781 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐹‘𝑋)) |