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

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 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 𝐹 ) ) ) )