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

Metamath Proof Explorer

Theorem dprdfsub

Description: Take the difference of group sums over two families 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 ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
dprdfadd.4 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
dprdfsub.b ⊢ − = ( -g ‘ 𝐺 )
Assertion dprdfsub ( 𝜑 → ( ( 𝐹 ∘f − 𝐻 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( ( 𝐺 Σ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 dprdfadd.4 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
7 dprdfsub.b ⊢ − = ( -g ‘ 𝐺 )
8 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
9 2 3 4 5 8 dprdff ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
10 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
11 2 3 4 6 8 dprdff ⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
12 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
13 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
14 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
15 8 13 14 7 grpsubval ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐻 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
16 10 12 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
17 16 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
18 3 4 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
19 9 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) )
20 11 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑘 ∈ 𝐼 ↦ ( 𝐻 ‘ 𝑘 ) ) )
21 18 10 12 19 20 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) = ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) ) )
22 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ∈ V )
23 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
24 3 23 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
25 8 14 24 grpinvf1o ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐺 ) )
26 f1of ⊢ ( ( invg ‘ 𝐺 ) : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐺 ) → ( invg ‘ 𝐺 ) : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
27 25 26 syl ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
28 27 feqmptd ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) )
29 fveq2 ⊢ ( 𝑥 = ( 𝐻 ‘ 𝑘 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) )
30 12 20 28 29 fmptco ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) = ( 𝑘 ∈ 𝐼 ↦ ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
31 18 10 22 19 30 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
32 17 21 31 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) = ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) )
33 1 2 3 4 6 14 dprdfinv ⊢ ( 𝜑 → ( ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
34 33 simpld ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ∈ 𝑊 )
35 1 2 3 4 5 34 13 dprdfadd ⊢ ( 𝜑 → ( ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) ) )
36 35 simpld ⊢ ( 𝜑 → ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ∈ 𝑊 )
37 32 36 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) ∈ 𝑊 )
38 32 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( 𝐺 Σg ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) )
39 33 simprd ⊢ ( 𝜑 → ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) )
40 39 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
41 35 simprd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) )
42 8 dprdssv ⊢ ( 𝐺 DProd 𝑆 ) ⊆ ( Base ‘ 𝐺 )
43 1 2 3 4 5 eldprdi ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) )
44 42 43 sselid ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( Base ‘ 𝐺 ) )
45 1 2 3 4 6 eldprdi ⊢ ( 𝜑 → ( 𝐺 Σg 𝐻 ) ∈ ( 𝐺 DProd 𝑆 ) )
46 42 45 sselid ⊢ ( 𝜑 → ( 𝐺 Σg 𝐻 ) ∈ ( Base ‘ 𝐺 ) )
47 8 13 14 7 grpsubval ⊢ ( ( ( 𝐺 Σg 𝐹 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐺 Σg 𝐻 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
48 44 46 47 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
49 40 41 48 3eqtr4d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )
50 38 49 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )
51 37 50 jca ⊢ ( 𝜑 → ( ( 𝐹 ∘f − 𝐻 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) ) )