This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumunsnfd

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumunsnd.b ⊢ B = Base G
gsumunsnd.p ⊢ + ˙ = + G
gsumunsnd.g ⊢ φ → G ∈ CMnd
gsumunsnd.a ⊢ φ → A ∈ Fin
gsumunsnd.f ⊢ φ ∧ k ∈ A → X ∈ B
gsumunsnd.m ⊢ φ → M ∈ V
gsumunsnd.d ⊢ φ → ¬ M ∈ A
gsumunsnd.y ⊢ φ → Y ∈ B
gsumunsnd.s ⊢ φ ∧ k = M → X = Y
gsumunsnfd.0 ⊢ Ⅎ _ k Y
Assertion gsumunsnfd ⊢ φ → ∑ G k ∈ A ∪ M X = ∑ G k ∈ A X + ˙ Y

Proof

Step Hyp Ref Expression
1 gsumunsnd.b ⊢ B = Base G
2 gsumunsnd.p ⊢ + ˙ = + G
3 gsumunsnd.g ⊢ φ → G ∈ CMnd
4 gsumunsnd.a ⊢ φ → A ∈ Fin
5 gsumunsnd.f ⊢ φ ∧ k ∈ A → X ∈ B
6 gsumunsnd.m ⊢ φ → M ∈ V
7 gsumunsnd.d ⊢ φ → ¬ M ∈ A
8 gsumunsnd.y ⊢ φ → Y ∈ B
9 gsumunsnd.s ⊢ φ ∧ k = M → X = Y
10 gsumunsnfd.0 ⊢ Ⅎ _ k Y
11 snfi ⊢ M ∈ Fin
12 unfi ⊢ A ∈ Fin ∧ M ∈ Fin → A ∪ M ∈ Fin
13 4 11 12 sylancl ⊢ φ → A ∪ M ∈ Fin
14 elun ⊢ k ∈ A ∪ M ↔ k ∈ A ∨ k ∈ M
15 elsni ⊢ k ∈ M → k = M
16 15 9 sylan2 ⊢ φ ∧ k ∈ M → X = Y
17 8 adantr ⊢ φ ∧ k ∈ M → Y ∈ B
18 16 17 eqeltrd ⊢ φ ∧ k ∈ M → X ∈ B
19 5 18 jaodan ⊢ φ ∧ k ∈ A ∨ k ∈ M → X ∈ B
20 14 19 sylan2b ⊢ φ ∧ k ∈ A ∪ M → X ∈ B
21 disjsn ⊢ A ∩ M = ∅ ↔ ¬ M ∈ A
22 7 21 sylibr ⊢ φ → A ∩ M = ∅
23 eqidd ⊢ φ → A ∪ M = A ∪ M
24 1 2 3 13 20 22 23 gsummptfidmsplit ⊢ φ → ∑ G k ∈ A ∪ M X = ∑ G k ∈ A X + ˙ ∑ G k ∈ M X
25 cmnmnd ⊢ G ∈ CMnd → G ∈ Mnd
26 3 25 syl ⊢ φ → G ∈ Mnd
27 nfv ⊢ Ⅎ k φ
28 1 26 6 8 9 27 10 gsumsnfd ⊢ φ → ∑ G k ∈ M X = Y
29 28 oveq2d ⊢ φ → ∑ G k ∈ A X + ˙ ∑ G k ∈ M X = ∑ G k ∈ A X + ˙ Y
30 24 29 eqtrd ⊢ φ → ∑ G k ∈ A ∪ M X = ∑ G k ∈ A X + ˙ Y