Metamath Proof Explorer

Theorem dmdprdsplitlem

Description: Lemma for dmdprdsplit . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses dmdprdsplitlem.0 ⊢0˙=0G
dmdprdsplitlem.w ⊢W=h∈⨉i∈IS⁡i|finSupp0˙⁡h
dmdprdsplitlem.1 ⊢φ→Gdom⁡DProdS
dmdprdsplitlem.2 ⊢φ→dom⁡S=I
dmdprdsplitlem.3 ⊢φ→A⊆I
dmdprdsplitlem.4 ⊢φ→F∈W
dmdprdsplitlem.5 ⊢φ→∑GF∈GDProdS↾A
Assertion dmdprdsplitlem ⊢φ∧X∈I∖A→F⁡X=0˙

Proof

Step Hyp Ref Expression
1 dmdprdsplitlem.0 ⊢0˙=0G
2 dmdprdsplitlem.w ⊢W=h∈⨉i∈IS⁡i|finSupp0˙⁡h
3 dmdprdsplitlem.1 ⊢φ→Gdom⁡DProdS
4 dmdprdsplitlem.2 ⊢φ→dom⁡S=I
5 dmdprdsplitlem.3 ⊢φ→A⊆I
6 dmdprdsplitlem.4 ⊢φ→F∈W
7 dmdprdsplitlem.5 ⊢φ→∑GF∈GDProdS↾A
8 3 4 dprdf2 ⊢φ→S:I⟶SubGrp⁡G
9 8 5 fssresd ⊢φ→S↾A:A⟶SubGrp⁡G
10 fdm ⊢S↾A:A⟶SubGrp⁡G→dom⁡S↾A=A
11 eqid ⊢h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h=h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h
12 1 11 eldprd ⊢dom⁡S↾A=A→∑GF∈GDProdS↾A↔Gdom⁡DProdS↾A∧∃f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∑GF=∑Gf
13 9 10 12 3syl ⊢φ→∑GF∈GDProdS↾A↔Gdom⁡DProdS↾A∧∃f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∑GF=∑Gf
14 7 13 mpbid ⊢φ→Gdom⁡DProdS↾A∧∃f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∑GF=∑Gf
15 14 simprd ⊢φ→∃f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∑GF=∑Gf
16 15 adantr ⊢φ∧X∈I∖A→∃f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∑GF=∑Gf
17 simprr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→∑GF=∑Gf
18 14 simpld ⊢φ→Gdom⁡DProdS↾A
19 18 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→Gdom⁡DProdS↾A
20 9 10 syl ⊢φ→dom⁡S↾A=A
21 20 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→dom⁡S↾A=A
22 simprl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h
23 eqid ⊢BaseG=BaseG
24 11 19 21 22 23 dprdff ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→f:A⟶BaseG
25 24 feqmptd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→f=n∈A⟼f⁡n
26 5 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→A⊆I
27 26 resmptd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙↾A=n∈A⟼ifn∈Af⁡n0˙
28 iftrue ⊢n∈A→ifn∈Af⁡n0˙=f⁡n
29 28 mpteq2ia ⊢n∈A⟼ifn∈Af⁡n0˙=n∈A⟼f⁡n
30 27 29 eqtrdi ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙↾A=n∈A⟼f⁡n
31 25 30 eqtr4d ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→f=n∈I⟼ifn∈Af⁡n0˙↾A
32 31 oveq2d ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→∑Gf=∑Gn∈I⟼ifn∈Af⁡n0˙↾A
33 eqid ⊢Cntz⁡G=Cntz⁡G
34 3 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→Gdom⁡DProdS
35 dprdgrp ⊢Gdom⁡DProdS→G∈Grp
36 grpmnd ⊢G∈Grp→G∈Mnd
37 34 35 36 3syl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→G∈Mnd
38 3 4 dprddomcld ⊢φ→I∈V
39 38 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→I∈V
40 4 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→dom⁡S=I
41 19 adantr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I→Gdom⁡DProdS↾A
42 21 adantr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I→dom⁡S↾A=A
43 simplrl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I→f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h
44 11 41 42 43 dprdfcl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∧n∈A→f⁡n∈S↾A⁡n
45 fvres ⊢n∈A→S↾A⁡n=S⁡n
46 45 adantl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∧n∈A→S↾A⁡n=S⁡n
47 44 46 eleqtrd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∧n∈A→f⁡n∈S⁡n
48 8 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→S:I⟶SubGrp⁡G
49 48 ffvelcdmda ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I→S⁡n∈SubGrp⁡G
50 1 subg0cl ⊢S⁡n∈SubGrp⁡G→0˙∈S⁡n
51 49 50 syl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I→0˙∈S⁡n
52 51 adantr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∧¬n∈A→0˙∈S⁡n
53 47 52 ifclda ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I→ifn∈Af⁡n0˙∈S⁡n
54 38 mptexd ⊢φ→n∈I⟼ifn∈Af⁡n0˙∈V
55 54 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙∈V
56 funmpt ⊢Fun⁡n∈I⟼ifn∈Af⁡n0˙
57 56 a1i ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→Fun⁡n∈I⟼ifn∈Af⁡n0˙
58 11 19 21 22 dprdffsupp ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→finSupp0˙⁡f
59 simpr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖supp0˙⁡f∧n∈A→n∈A
60 eldifn ⊢n∈I∖supp0˙⁡f→¬n∈supp0˙⁡f
61 60 ad2antlr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖supp0˙⁡f∧n∈A→¬n∈supp0˙⁡f
62 59 61 eldifd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖supp0˙⁡f∧n∈A→n∈A∖supp0˙⁡f
63 ssidd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→fsupp0˙⊆fsupp0˙
64 38 5 ssexd ⊢φ→A∈V
65 64 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→A∈V
66 1 fvexi ⊢0˙∈V
67 66 a1i ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→0˙∈V
68 24 63 65 67 suppssr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈A∖supp0˙⁡f→f⁡n=0˙
69 68 adantlr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖supp0˙⁡f∧n∈A∖supp0˙⁡f→f⁡n=0˙
70 62 69 syldan ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖supp0˙⁡f∧n∈A→f⁡n=0˙
71 70 ifeq1da ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖supp0˙⁡f→ifn∈Af⁡n0˙=ifn∈A0˙0˙
72 ifid ⊢ifn∈A0˙0˙=0˙
73 71 72 eqtrdi ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖supp0˙⁡f→ifn∈Af⁡n0˙=0˙
74 73 39 suppss2 ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙supp0˙⊆fsupp0˙
75 fsuppsssupp ⊢n∈I⟼ifn∈Af⁡n0˙∈V∧Fun⁡n∈I⟼ifn∈Af⁡n0˙∧finSupp0˙⁡f∧n∈I⟼ifn∈Af⁡n0˙supp0˙⊆fsupp0˙→finSupp0˙⁡n∈I⟼ifn∈Af⁡n0˙
76 55 57 58 74 75 syl22anc ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→finSupp0˙⁡n∈I⟼ifn∈Af⁡n0˙
77 2 34 40 53 76 dprdwd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙∈W
78 2 34 40 77 23 dprdff ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙:I⟶BaseG
79 2 34 40 77 33 dprdfcntz ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→ran⁡n∈I⟼ifn∈Af⁡n0˙⊆Cntz⁡G⁡ran⁡n∈I⟼ifn∈Af⁡n0˙
80 eldifn ⊢n∈I∖A→¬n∈A
81 80 adantl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖A→¬n∈A
82 81 iffalsed ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf∧n∈I∖A→ifn∈Af⁡n0˙=0˙
83 82 39 suppss2 ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙supp0˙⊆A
84 23 1 33 37 39 78 79 83 76 gsumzres ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→∑Gn∈I⟼ifn∈Af⁡n0˙↾A=∑Gn∈Iifn∈Af⁡n0˙
85 17 32 84 3eqtrd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→∑GF=∑Gn∈Iifn∈Af⁡n0˙
86 6 ad2antrr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→F∈W
87 1 2 34 40 86 77 dprdf11 ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→∑GF=∑Gn∈Iifn∈Af⁡n0˙↔F=n∈I⟼ifn∈Af⁡n0˙
88 85 87 mpbid ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→F=n∈I⟼ifn∈Af⁡n0˙
89 88 fveq1d ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→F⁡X=n∈I⟼ifn∈Af⁡n0˙⁡X
90 eldifi ⊢X∈I∖A→X∈I
91 90 ad2antlr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→X∈I
92 eleq1 ⊢n=X→n∈A↔X∈A
93 fveq2 ⊢n=X→f⁡n=f⁡X
94 92 93 ifbieq1d ⊢n=X→ifn∈Af⁡n0˙=ifX∈Af⁡X0˙
95 eqid ⊢n∈I⟼ifn∈Af⁡n0˙=n∈I⟼ifn∈Af⁡n0˙
96 fvex ⊢f⁡n∈V
97 96 66 ifex ⊢ifn∈Af⁡n0˙∈V
98 94 95 97 fvmpt3i ⊢X∈I→n∈I⟼ifn∈Af⁡n0˙⁡X=ifX∈Af⁡X0˙
99 91 98 syl ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→n∈I⟼ifn∈Af⁡n0˙⁡X=ifX∈Af⁡X0˙
100 eldifn ⊢X∈I∖A→¬X∈A
101 100 ad2antlr ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→¬X∈A
102 101 iffalsed ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→ifX∈Af⁡X0˙=0˙
103 89 99 102 3eqtrd ⊢φ∧X∈I∖A∧f∈h∈⨉i∈AS↾A⁡i|finSupp0˙⁡h∧∑GF=∑Gf→F⁡X=0˙
104 16 103 rexlimddv ⊢φ∧X∈I∖A→F⁡X=0˙