| Step | Hyp | Ref
| Expression |
| 1 | | gsumpt.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 2 | | gsumpt.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
| 3 | 2 | snssd 4809 |
. . . 4
⊢ (𝜑 → {𝑋} ⊆ 𝐴) |
| 4 | 1, 3 | feqresmpt 6978 |
. . 3
⊢ (𝜑 → (𝐹 ↾ {𝑋}) = (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) |
| 5 | 4 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ {𝑋})) = (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎)))) |
| 6 | | gsumpt.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
| 7 | | gsumpt.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
| 8 | | eqid 2737 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
| 9 | | gsumpt.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
| 10 | | gsumpt.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 11 | 1, 2 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵) |
| 12 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))) |
| 13 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 14 | 6, 13, 8 | elcntzsn 19343 |
. . . . . . . . 9
⊢ ((𝐹‘𝑋) ∈ 𝐵 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
| 15 | 11, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)}) ↔ ((𝐹‘𝑋) ∈ 𝐵 ∧ ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋)) = ((𝐹‘𝑋)(+g‘𝐺)(𝐹‘𝑋))))) |
| 16 | 11, 12, 15 | mpbir2and 713 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) |
| 17 | 16 | snssd 4809 |
. . . . . 6
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) |
| 18 | | eqid 2737 |
. . . . . . 7
⊢
(mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺)) |
| 19 | | eqid 2737 |
. . . . . . 7
⊢ (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) = (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 20 | 8, 18, 19 | cntzspan 19862 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ {(𝐹‘𝑋)} ⊆ ((Cntz‘𝐺)‘{(𝐹‘𝑋)})) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
| 21 | 9, 17, 20 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) ∈ CMnd) |
| 22 | 6 | submacs 18840 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
| 23 | | acsmre 17695 |
. . . . . . . 8
⊢
((SubMnd‘𝐺)
∈ (ACS‘𝐵) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
| 24 | 9, 22, 23 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (SubMnd‘𝐺) ∈ (Moore‘𝐵)) |
| 25 | 11 | snssd 4809 |
. . . . . . 7
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ 𝐵) |
| 26 | 18 | mrccl 17654 |
. . . . . . 7
⊢
(((SubMnd‘𝐺)
∈ (Moore‘𝐵)
∧ {(𝐹‘𝑋)} ⊆ 𝐵) → ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
| 27 | 24, 25, 26 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺)) |
| 28 | 19, 8 | submcmn2 19857 |
. . . . . 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 232 |
. . . 4
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ⊆ ((Cntz‘𝐺)‘((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
| 31 | 1 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝐴) |
| 32 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → 𝑎 = 𝑋) |
| 33 | 32 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) = (𝐹‘𝑋)) |
| 34 | 24, 18, 25 | mrcssidd 17668 |
. . . . . . . . . . 11
⊢ (𝜑 → {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 35 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑋) ∈ V |
| 36 | 35 | snss 4785 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ {(𝐹‘𝑋)} ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 37 | 34, 36 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 38 | 37 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑋) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 39 | 33, 38 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 = 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 40 | | eldifsn 4786 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝐴 ∖ {𝑋}) ↔ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) |
| 41 | | gsumpt.s |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ {𝑋}) |
| 42 | 7 | fvexi 6920 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
| 43 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ V) |
| 44 | 1, 41, 10, 43 | suppssr 8220 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 ∖ {𝑋})) → (𝐹‘𝑎) = 0 ) |
| 45 | 40, 44 | sylan2br 595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) = 0 ) |
| 46 | 7 | subm0cl 18824 |
. . . . . . . . . . . 12
⊢
(((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ∈ (SubMnd‘𝐺) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 47 | 27, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 48 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 49 | 45, 48 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑎 ≠ 𝑋)) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 50 | 49 | anassrs 467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 ≠ 𝑋) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 51 | 39, 50 | pm2.61dane 3029 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 52 | 51 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 53 | | ffnfv 7139 |
. . . . . 6
⊢ (𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) ∈ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)}))) |
| 54 | 31, 52, 53 | sylanbrc 583 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 55 | 54 | frnd 6744 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘{(𝐹‘𝑋)})) |
| 56 | 8 | cntzidss 19358 |
. . . 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 6740 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
| 59 | | snfi 9083 |
. . . . 5
⊢ {𝑋} ∈ Fin |
| 60 | | ssfi 9213 |
. . . . 5
⊢ (({𝑋} ∈ Fin ∧ (𝐹 supp 0 ) ⊆ {𝑋}) → (𝐹 supp 0 ) ∈
Fin) |
| 61 | 59, 41, 60 | sylancr 587 |
. . . 4
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
| 62 | 1, 10 | fexd 7247 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ V) |
| 63 | | isfsupp 9405 |
. . . . 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 713 |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
| 66 | 6, 7, 8, 9, 10, 1,
57, 41, 65 | gsumzres 19927 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ {𝑋})) = (𝐺 Σg 𝐹)) |
| 67 | | fveq2 6906 |
. . . 4
⊢ (𝑎 = 𝑋 → (𝐹‘𝑎) = (𝐹‘𝑋)) |
| 68 | 6, 67 | gsumsn 19972 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ 𝐵) → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
| 69 | 9, 2, 11, 68 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑎 ∈ {𝑋} ↦ (𝐹‘𝑎))) = (𝐹‘𝑋)) |
| 70 | 5, 66, 69 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐹‘𝑋)) |