Metamath Proof Explorer


Theorem dprdfinv

Description: Take the inverse of a group sum over a family of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 0 = ( 0g𝐺 )
eldprdi.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
eldprdi.1 ( 𝜑𝐺 dom DProd 𝑆 )
eldprdi.2 ( 𝜑 → dom 𝑆 = 𝐼 )
eldprdi.3 ( 𝜑𝐹𝑊 )
dprdfinv.b 𝑁 = ( invg𝐺 )
Assertion dprdfinv ( 𝜑 → ( ( 𝑁𝐹 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝑁𝐹 ) ) = ( 𝑁 ‘ ( 𝐺 Σg 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 0 = ( 0g𝐺 )
2 eldprdi.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
3 eldprdi.1 ( 𝜑𝐺 dom DProd 𝑆 )
4 eldprdi.2 ( 𝜑 → dom 𝑆 = 𝐼 )
5 eldprdi.3 ( 𝜑𝐹𝑊 )
6 dprdfinv.b 𝑁 = ( invg𝐺 )
7 dprdgrp ( 𝐺 dom DProd 𝑆𝐺 ∈ Grp )
8 3 7 syl ( 𝜑𝐺 ∈ Grp )
9 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10 9 6 grpinvf ( 𝐺 ∈ Grp → 𝑁 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
11 8 10 syl ( 𝜑𝑁 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
12 2 3 4 5 9 dprdff ( 𝜑𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
13 fcompt ( ( 𝑁 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) ∧ 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) ) → ( 𝑁𝐹 ) = ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) )
14 11 12 13 syl2anc ( 𝜑 → ( 𝑁𝐹 ) = ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) )
15 3 4 dprdf2 ( 𝜑𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
16 15 ffvelrnda ( ( 𝜑𝑥𝐼 ) → ( 𝑆𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
17 2 3 4 5 dprdfcl ( ( 𝜑𝑥𝐼 ) → ( 𝐹𝑥 ) ∈ ( 𝑆𝑥 ) )
18 6 subginvcl ( ( ( 𝑆𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐹𝑥 ) ∈ ( 𝑆𝑥 ) ) → ( 𝑁 ‘ ( 𝐹𝑥 ) ) ∈ ( 𝑆𝑥 ) )
19 16 17 18 syl2anc ( ( 𝜑𝑥𝐼 ) → ( 𝑁 ‘ ( 𝐹𝑥 ) ) ∈ ( 𝑆𝑥 ) )
20 3 4 dprddomcld ( 𝜑𝐼 ∈ V )
21 20 mptexd ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) ∈ V )
22 funmpt Fun ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) )
23 22 a1i ( 𝜑 → Fun ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) )
24 2 3 4 5 dprdffsupp ( 𝜑𝐹 finSupp 0 )
25 ssidd ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
26 1 fvexi 0 ∈ V
27 26 a1i ( 𝜑0 ∈ V )
28 12 25 20 27 suppssr ( ( 𝜑𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹𝑥 ) = 0 )
29 28 fveq2d ( ( 𝜑𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑁 ‘ ( 𝐹𝑥 ) ) = ( 𝑁0 ) )
30 1 6 grpinvid ( 𝐺 ∈ Grp → ( 𝑁0 ) = 0 )
31 8 30 syl ( 𝜑 → ( 𝑁0 ) = 0 )
32 31 adantr ( ( 𝜑𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑁0 ) = 0 )
33 29 32 eqtrd ( ( 𝜑𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑁 ‘ ( 𝐹𝑥 ) ) = 0 )
34 33 20 suppss2 ( 𝜑 → ( ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
35 fsuppsssupp ( ( ( ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) ∈ V ∧ Fun ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) ) ∧ ( 𝐹 finSupp 0 ∧ ( ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) ) → ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) finSupp 0 )
36 21 23 24 34 35 syl22anc ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) finSupp 0 )
37 2 3 4 19 36 dprdwd ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝑁 ‘ ( 𝐹𝑥 ) ) ) ∈ 𝑊 )
38 14 37 eqeltrd ( 𝜑 → ( 𝑁𝐹 ) ∈ 𝑊 )
39 eqid ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
40 2 3 4 5 39 dprdfcntz ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
41 9 1 39 6 8 20 12 40 24 gsumzinv ( 𝜑 → ( 𝐺 Σg ( 𝑁𝐹 ) ) = ( 𝑁 ‘ ( 𝐺 Σg 𝐹 ) ) )
42 38 41 jca ( 𝜑 → ( ( 𝑁𝐹 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝑁𝐹 ) ) = ( 𝑁 ‘ ( 𝐺 Σg 𝐹 ) ) ) )