Metamath Proof Explorer

Theorem gsummulglem

Description: Lemma for gsummulg and gsummulgz . (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsummulg.b ⊢ B = Base G
gsummulg.z ⊢ 0 ˙ = 0 G
gsummulg.t ⊢ · ˙ = ⋅ G
gsummulg.a ⊢ φ → A ∈ V
gsummulg.f ⊢ φ ∧ k ∈ A → X ∈ B
gsummulg.w ⊢ φ → finSupp 0 ˙⁡ k ∈ A ⟼ X
gsummulglem.g ⊢ φ → G ∈ CMnd
gsummulglem.n ⊢ φ → N ∈ ℤ
gsummulglem.o ⊢ φ → G ∈ Abel ∨ N ∈ ℕ 0
Assertion gsummulglem ⊢ φ → ∑ G k ∈ A N · ˙ X = N · ˙ ∑ G k ∈ A X

Proof

Step Hyp Ref Expression
1 gsummulg.b ⊢ B = Base G
2 gsummulg.z ⊢ 0 ˙ = 0 G
3 gsummulg.t ⊢ · ˙ = ⋅ G
4 gsummulg.a ⊢ φ → A ∈ V
5 gsummulg.f ⊢ φ ∧ k ∈ A → X ∈ B
6 gsummulg.w ⊢ φ → finSupp 0 ˙⁡ k ∈ A ⟼ X
7 gsummulglem.g ⊢ φ → G ∈ CMnd
8 gsummulglem.n ⊢ φ → N ∈ ℤ
9 gsummulglem.o ⊢ φ → G ∈ Abel ∨ N ∈ ℕ 0
10 cmnmnd ⊢ G ∈ CMnd → G ∈ Mnd
11 7 10 syl ⊢ φ → G ∈ Mnd
12 1 3 mulgghm ⊢ G ∈ Abel ∧ N ∈ ℤ → x ∈ B ⟼ N · ˙ x ∈ G GrpHom G
13 ghmmhm ⊢ x ∈ B ⟼ N · ˙ x ∈ G GrpHom G → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
14 12 13 syl ⊢ G ∈ Abel ∧ N ∈ ℤ → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
15 14 expcom ⊢ N ∈ ℤ → G ∈ Abel → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
16 8 15 syl ⊢ φ → G ∈ Abel → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
17 1 3 mulgmhm ⊢ G ∈ CMnd ∧ N ∈ ℕ 0 → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
18 17 ex ⊢ G ∈ CMnd → N ∈ ℕ 0 → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
19 7 18 syl ⊢ φ → N ∈ ℕ 0 → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
20 16 19 9 mpjaod ⊢ φ → x ∈ B ⟼ N · ˙ x ∈ G MndHom G
21 oveq2 ⊢ x = X → N · ˙ x = N · ˙ X
22 oveq2 ⊢ x = ∑ G k ∈ A X → N · ˙ x = N · ˙ ∑ G k ∈ A X
23 1 2 7 11 4 20 5 6 21 22 gsummhm2 ⊢ φ → ∑ G k ∈ A N · ˙ X = N · ˙ ∑ G k ∈ A X