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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
11	2 3 4 6 8	dprdff	⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
12	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) ∈ ( 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 𝐻 ) ) ) )