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 ˙ = 0 G
dmdprdsplitlem.w W = h i I S i | finSupp 0 ˙ h
dmdprdsplitlem.1 φ G dom DProd S
dmdprdsplitlem.2 φ dom S = I
dmdprdsplitlem.3 φ A I
dmdprdsplitlem.4 φ F W
dmdprdsplitlem.5 φ G F G DProd S A
Assertion dmdprdsplitlem φ X I A F X = 0 ˙

Proof

Step Hyp Ref Expression
1 dmdprdsplitlem.0 0 ˙ = 0 G
2 dmdprdsplitlem.w W = h i I S i | finSupp 0 ˙ h
3 dmdprdsplitlem.1 φ G dom DProd S
4 dmdprdsplitlem.2 φ dom S = I
5 dmdprdsplitlem.3 φ A I
6 dmdprdsplitlem.4 φ F W
7 dmdprdsplitlem.5 φ G F G DProd S 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 A S A i | finSupp 0 ˙ h = h i A S A i | finSupp 0 ˙ h
12 1 11 eldprd dom S A = A G F G DProd S A G dom DProd S A f h i A S A i | finSupp 0 ˙ h G F = G f
13 9 10 12 3syl φ G F G DProd S A G dom DProd S A f h i A S A i | finSupp 0 ˙ h G F = G f
14 7 13 mpbid φ G dom DProd S A f h i A S A i | finSupp 0 ˙ h G F = G f
15 14 simprd φ f h i A S A i | finSupp 0 ˙ h G F = G f
16 15 adantr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f
17 simprr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G F = G f
18 14 simpld φ G dom DProd S A
19 18 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G dom DProd S A
20 9 10 syl φ dom S A = A
21 20 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f dom S A = A
22 simprl φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f f h i A S A i | finSupp 0 ˙ h
23 eqid Base G = Base G
24 11 19 21 22 23 dprdff φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f f : A Base G
25 24 feqmptd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f f = n A f n
26 5 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f A I
27 26 resmptd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ A = n A if n A f n 0 ˙
28 iftrue n A if n A f n 0 ˙ = f n
29 28 mpteq2ia n A if n A f n 0 ˙ = n A f n
30 27 29 eqtrdi φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ A = n A f n
31 25 30 eqtr4d φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f f = n I if n A f n 0 ˙ A
32 31 oveq2d φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G f = G n I if n A f n 0 ˙ A
33 eqid Cntz G = Cntz G
34 3 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G dom DProd S
35 dprdgrp G dom DProd S G Grp
36 grpmnd G Grp G Mnd
37 34 35 36 3syl φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G Mnd
38 3 4 dprddomcld φ I V
39 38 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f I V
40 4 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f dom S = I
41 19 adantr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I G dom DProd S A
42 21 adantr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I dom S A = A
43 simplrl φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I f h i A S A i | finSupp 0 ˙ h
44 11 41 42 43 dprdfcl φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f 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 A S A i | finSupp 0 ˙ h G F = G f n I n A S A n = S n
47 44 46 eleqtrd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I n A f n S n
48 8 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f S : I SubGrp G
49 48 ffvelrnda φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f 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 A S A i | finSupp 0 ˙ h G F = G f n I 0 ˙ S n
52 51 adantr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I ¬ n A 0 ˙ S n
53 47 52 ifclda φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ S n
54 38 mptexd φ n I if n A f n 0 ˙ V
55 54 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ V
56 funmpt Fun n I if n A f n 0 ˙
57 56 a1i φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f Fun n I if n A f n 0 ˙
58 11 19 21 22 dprdffsupp φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f finSupp 0 ˙ f
59 simpr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I supp 0 ˙ f n A n A
60 eldifn n I supp 0 ˙ f ¬ n supp 0 ˙ f
61 60 ad2antlr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I supp 0 ˙ f n A ¬ n supp 0 ˙ f
62 59 61 eldifd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I supp 0 ˙ f n A n A supp 0 ˙ f
63 ssidd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f f supp 0 ˙ f supp 0 ˙
64 38 5 ssexd φ A V
65 64 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f A V
66 1 fvexi 0 ˙ V
67 66 a1i φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f 0 ˙ V
68 24 63 65 67 suppssr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n A supp 0 ˙ f f n = 0 ˙
69 68 adantlr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I supp 0 ˙ f n A supp 0 ˙ f f n = 0 ˙
70 62 69 syldan φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I supp 0 ˙ f n A f n = 0 ˙
71 70 ifeq1da φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I supp 0 ˙ f if n A f n 0 ˙ = if n A 0 ˙ 0 ˙
72 ifid if n A 0 ˙ 0 ˙ = 0 ˙
73 71 72 eqtrdi φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I supp 0 ˙ f if n A f n 0 ˙ = 0 ˙
74 73 39 suppss2 φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ supp 0 ˙ f supp 0 ˙
75 fsuppsssupp n I if n A f n 0 ˙ V Fun n I if n A f n 0 ˙ finSupp 0 ˙ f n I if n A f n 0 ˙ supp 0 ˙ f supp 0 ˙ finSupp 0 ˙ n I if n A f n 0 ˙
76 55 57 58 74 75 syl22anc φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f finSupp 0 ˙ n I if n A f n 0 ˙
77 2 34 40 53 76 dprdwd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ W
78 2 34 40 77 23 dprdff φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ : I Base G
79 2 34 40 77 33 dprdfcntz φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f ran n I if n A f n 0 ˙ Cntz G ran n I if n A f n 0 ˙
80 eldifn n I A ¬ n A
81 80 adantl φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I A ¬ n A
82 81 iffalsed φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I A if n A f n 0 ˙ = 0 ˙
83 82 39 suppss2 φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ supp 0 ˙ A
84 23 1 33 37 39 78 79 83 76 gsumzres φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G n I if n A f n 0 ˙ A = G n I if n A f n 0 ˙
85 17 32 84 3eqtrd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G F = G n I if n A f n 0 ˙
86 6 ad2antrr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f F W
87 1 2 34 40 86 77 dprdf11 φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f G F = G n I if n A f n 0 ˙ F = n I if n A f n 0 ˙
88 85 87 mpbid φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f F = n I if n A f n 0 ˙
89 88 fveq1d φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f F X = n I if n A f n 0 ˙ X
90 eldifi X I A X I
91 90 ad2antlr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f X I
92 eleq1 n = X n A X A
93 fveq2 n = X f n = f X
94 92 93 ifbieq1d n = X if n A f n 0 ˙ = if X A f X 0 ˙
95 eqid n I if n A f n 0 ˙ = n I if n A f n 0 ˙
96 fvex f n V
97 96 66 ifex if n A f n 0 ˙ V
98 94 95 97 fvmpt3i X I n I if n A f n 0 ˙ X = if X A f X 0 ˙
99 91 98 syl φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f n I if n A f n 0 ˙ X = if X A f X 0 ˙
100 eldifn X I A ¬ X A
101 100 ad2antlr φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f ¬ X A
102 101 iffalsed φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f if X A f X 0 ˙ = 0 ˙
103 89 99 102 3eqtrd φ X I A f h i A S A i | finSupp 0 ˙ h G F = G f F X = 0 ˙
104 16 103 rexlimddv φ X I A F X = 0 ˙