Metamath Proof Explorer


Theorem gsumzsplit

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumzsplit.b B = Base G
gsumzsplit.0 0 ˙ = 0 G
gsumzsplit.p + ˙ = + G
gsumzsplit.z Z = Cntz G
gsumzsplit.g φ G Mnd
gsumzsplit.a φ A V
gsumzsplit.f φ F : A B
gsumzsplit.c φ ran F Z ran F
gsumzsplit.w φ finSupp 0 ˙ F
gsumzsplit.i φ C D =
gsumzsplit.u φ A = C D
Assertion gsumzsplit φ G F = G F C + ˙ G F D

Proof

Step Hyp Ref Expression
1 gsumzsplit.b B = Base G
2 gsumzsplit.0 0 ˙ = 0 G
3 gsumzsplit.p + ˙ = + G
4 gsumzsplit.z Z = Cntz G
5 gsumzsplit.g φ G Mnd
6 gsumzsplit.a φ A V
7 gsumzsplit.f φ F : A B
8 gsumzsplit.c φ ran F Z ran F
9 gsumzsplit.w φ finSupp 0 ˙ F
10 gsumzsplit.i φ C D =
11 gsumzsplit.u φ A = C D
12 2 fvexi 0 ˙ V
13 12 a1i φ 0 ˙ V
14 7 6 13 9 fsuppmptif φ finSupp 0 ˙ k A if k C F k 0 ˙
15 7 6 13 9 fsuppmptif φ finSupp 0 ˙ k A if k D F k 0 ˙
16 1 submacs G Mnd SubMnd G ACS B
17 acsmre SubMnd G ACS B SubMnd G Moore B
18 5 16 17 3syl φ SubMnd G Moore B
19 7 frnd φ ran F B
20 eqid mrCls SubMnd G = mrCls SubMnd G
21 20 mrccl SubMnd G Moore B ran F B mrCls SubMnd G ran F SubMnd G
22 18 19 21 syl2anc φ mrCls SubMnd G ran F SubMnd G
23 eqid G 𝑠 mrCls SubMnd G ran F = G 𝑠 mrCls SubMnd G ran F
24 4 20 23 cntzspan G Mnd ran F Z ran F G 𝑠 mrCls SubMnd G ran F CMnd
25 5 8 24 syl2anc φ G 𝑠 mrCls SubMnd G ran F CMnd
26 23 4 submcmn2 mrCls SubMnd G ran F SubMnd G G 𝑠 mrCls SubMnd G ran F CMnd mrCls SubMnd G ran F Z mrCls SubMnd G ran F
27 22 26 syl φ G 𝑠 mrCls SubMnd G ran F CMnd mrCls SubMnd G ran F Z mrCls SubMnd G ran F
28 25 27 mpbid φ mrCls SubMnd G ran F Z mrCls SubMnd G ran F
29 18 20 19 mrcssidd φ ran F mrCls SubMnd G ran F
30 29 adantr φ k A ran F mrCls SubMnd G ran F
31 7 ffnd φ F Fn A
32 fnfvelrn F Fn A k A F k ran F
33 31 32 sylan φ k A F k ran F
34 30 33 sseldd φ k A F k mrCls SubMnd G ran F
35 2 subm0cl mrCls SubMnd G ran F SubMnd G 0 ˙ mrCls SubMnd G ran F
36 22 35 syl φ 0 ˙ mrCls SubMnd G ran F
37 36 adantr φ k A 0 ˙ mrCls SubMnd G ran F
38 34 37 ifcld φ k A if k C F k 0 ˙ mrCls SubMnd G ran F
39 38 fmpttd φ k A if k C F k 0 ˙ : A mrCls SubMnd G ran F
40 34 37 ifcld φ k A if k D F k 0 ˙ mrCls SubMnd G ran F
41 40 fmpttd φ k A if k D F k 0 ˙ : A mrCls SubMnd G ran F
42 1 2 3 4 5 6 14 15 22 28 39 41 gsumzadd φ G k A if k C F k 0 ˙ + ˙ f k A if k D F k 0 ˙ = G k A if k C F k 0 ˙ + ˙ G k A if k D F k 0 ˙
43 7 feqmptd φ F = k A F k
44 iftrue k C if k C F k 0 ˙ = F k
45 44 adantl φ k A k C if k C F k 0 ˙ = F k
46 noel ¬ k
47 eleq2 C D = k C D k
48 46 47 mtbiri C D = ¬ k C D
49 10 48 syl φ ¬ k C D
50 49 adantr φ k A ¬ k C D
51 elin k C D k C k D
52 50 51 sylnib φ k A ¬ k C k D
53 imnan k C ¬ k D ¬ k C k D
54 52 53 sylibr φ k A k C ¬ k D
55 54 imp φ k A k C ¬ k D
56 55 iffalsed φ k A k C if k D F k 0 ˙ = 0 ˙
57 45 56 oveq12d φ k A k C if k C F k 0 ˙ + ˙ if k D F k 0 ˙ = F k + ˙ 0 ˙
58 7 ffvelrnda φ k A F k B
59 1 3 2 mndrid G Mnd F k B F k + ˙ 0 ˙ = F k
60 5 58 59 syl2an2r φ k A F k + ˙ 0 ˙ = F k
61 60 adantr φ k A k C F k + ˙ 0 ˙ = F k
62 57 61 eqtrd φ k A k C if k C F k 0 ˙ + ˙ if k D F k 0 ˙ = F k
63 54 con2d φ k A k D ¬ k C
64 63 imp φ k A k D ¬ k C
65 64 iffalsed φ k A k D if k C F k 0 ˙ = 0 ˙
66 iftrue k D if k D F k 0 ˙ = F k
67 66 adantl φ k A k D if k D F k 0 ˙ = F k
68 65 67 oveq12d φ k A k D if k C F k 0 ˙ + ˙ if k D F k 0 ˙ = 0 ˙ + ˙ F k
69 1 3 2 mndlid G Mnd F k B 0 ˙ + ˙ F k = F k
70 5 58 69 syl2an2r φ k A 0 ˙ + ˙ F k = F k
71 70 adantr φ k A k D 0 ˙ + ˙ F k = F k
72 68 71 eqtrd φ k A k D if k C F k 0 ˙ + ˙ if k D F k 0 ˙ = F k
73 11 eleq2d φ k A k C D
74 elun k C D k C k D
75 73 74 bitrdi φ k A k C k D
76 75 biimpa φ k A k C k D
77 62 72 76 mpjaodan φ k A if k C F k 0 ˙ + ˙ if k D F k 0 ˙ = F k
78 77 mpteq2dva φ k A if k C F k 0 ˙ + ˙ if k D F k 0 ˙ = k A F k
79 43 78 eqtr4d φ F = k A if k C F k 0 ˙ + ˙ if k D F k 0 ˙
80 1 2 mndidcl G Mnd 0 ˙ B
81 5 80 syl φ 0 ˙ B
82 81 adantr φ k A 0 ˙ B
83 58 82 ifcld φ k A if k C F k 0 ˙ B
84 58 82 ifcld φ k A if k D F k 0 ˙ B
85 eqidd φ k A if k C F k 0 ˙ = k A if k C F k 0 ˙
86 eqidd φ k A if k D F k 0 ˙ = k A if k D F k 0 ˙
87 6 83 84 85 86 offval2 φ k A if k C F k 0 ˙ + ˙ f k A if k D F k 0 ˙ = k A if k C F k 0 ˙ + ˙ if k D F k 0 ˙
88 79 87 eqtr4d φ F = k A if k C F k 0 ˙ + ˙ f k A if k D F k 0 ˙
89 88 oveq2d φ G F = G k A if k C F k 0 ˙ + ˙ f k A if k D F k 0 ˙
90 43 reseq1d φ F C = k A F k C
91 ssun1 C C D
92 91 11 sseqtrrid φ C A
93 44 mpteq2ia k C if k C F k 0 ˙ = k C F k
94 resmpt C A k A if k C F k 0 ˙ C = k C if k C F k 0 ˙
95 resmpt C A k A F k C = k C F k
96 93 94 95 3eqtr4a C A k A if k C F k 0 ˙ C = k A F k C
97 92 96 syl φ k A if k C F k 0 ˙ C = k A F k C
98 90 97 eqtr4d φ F C = k A if k C F k 0 ˙ C
99 98 oveq2d φ G F C = G k A if k C F k 0 ˙ C
100 83 fmpttd φ k A if k C F k 0 ˙ : A B
101 39 frnd φ ran k A if k C F k 0 ˙ mrCls SubMnd G ran F
102 4 cntzidss mrCls SubMnd G ran F Z mrCls SubMnd G ran F ran k A if k C F k 0 ˙ mrCls SubMnd G ran F ran k A if k C F k 0 ˙ Z ran k A if k C F k 0 ˙
103 28 101 102 syl2anc φ ran k A if k C F k 0 ˙ Z ran k A if k C F k 0 ˙
104 eldifn k A C ¬ k C
105 104 adantl φ k A C ¬ k C
106 105 iffalsed φ k A C if k C F k 0 ˙ = 0 ˙
107 106 6 suppss2 φ k A if k C F k 0 ˙ supp 0 ˙ C
108 1 2 4 5 6 100 103 107 14 gsumzres φ G k A if k C F k 0 ˙ C = G k A if k C F k 0 ˙
109 99 108 eqtrd φ G F C = G k A if k C F k 0 ˙
110 43 reseq1d φ F D = k A F k D
111 ssun2 D C D
112 111 11 sseqtrrid φ D A
113 66 mpteq2ia k D if k D F k 0 ˙ = k D F k
114 resmpt D A k A if k D F k 0 ˙ D = k D if k D F k 0 ˙
115 resmpt D A k A F k D = k D F k
116 113 114 115 3eqtr4a D A k A if k D F k 0 ˙ D = k A F k D
117 112 116 syl φ k A if k D F k 0 ˙ D = k A F k D
118 110 117 eqtr4d φ F D = k A if k D F k 0 ˙ D
119 118 oveq2d φ G F D = G k A if k D F k 0 ˙ D
120 84 fmpttd φ k A if k D F k 0 ˙ : A B
121 41 frnd φ ran k A if k D F k 0 ˙ mrCls SubMnd G ran F
122 4 cntzidss mrCls SubMnd G ran F Z mrCls SubMnd G ran F ran k A if k D F k 0 ˙ mrCls SubMnd G ran F ran k A if k D F k 0 ˙ Z ran k A if k D F k 0 ˙
123 28 121 122 syl2anc φ ran k A if k D F k 0 ˙ Z ran k A if k D F k 0 ˙
124 eldifn k A D ¬ k D
125 124 adantl φ k A D ¬ k D
126 125 iffalsed φ k A D if k D F k 0 ˙ = 0 ˙
127 126 6 suppss2 φ k A if k D F k 0 ˙ supp 0 ˙ D
128 1 2 4 5 6 120 123 127 15 gsumzres φ G k A if k D F k 0 ˙ D = G k A if k D F k 0 ˙
129 119 128 eqtrd φ G F D = G k A if k D F k 0 ˙
130 109 129 oveq12d φ G F C + ˙ G F D = G k A if k C F k 0 ˙ + ˙ G k A if k D F k 0 ˙
131 42 89 130 3eqtr4d φ G F = G F C + ˙ G F D