Theorem dprdfid

Description: A function mapping all but one arguments to zero sums to the value of this argument in a direct product. (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 𝑆 = 𝐼 )
	dprdfid.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	dprdfid.4	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) )
	dprdfid.f	⊢ 𝐹 = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
Assertion	dprdfid	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( 𝐺 Σ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		dprdfid.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
6		dprdfid.4	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) )
7		dprdfid.f	⊢ 𝐹 = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
8	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) )
9		simpr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → 𝑛 = 𝑋 )
10	9	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑋 ) )
11	8 10	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ 𝑛 = 𝑋 ) → 𝐴 ∈ ( 𝑆 ‘ 𝑛 ) )
12	3 4	dprdf2	⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
13	12	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑛 ) ∈ ( SubGrp ‘ 𝐺 ) )
14	1	subg0cl	⊢ ( ( 𝑆 ‘ 𝑛 ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑆 ‘ 𝑛 ) )
15	13 14	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 0 ∈ ( 𝑆 ‘ 𝑛 ) )
16	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ¬ 𝑛 = 𝑋 ) → 0 ∈ ( 𝑆 ‘ 𝑛 ) )
17	11 16	ifclda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ∈ ( 𝑆 ‘ 𝑛 ) )
18	3 4	dprddomcld	⊢ ( 𝜑 → 𝐼 ∈ V )
19	1	fvexi	⊢ 0 ∈ V
20	19	a1i	⊢ ( 𝜑 → 0 ∈ V )
21		eqid	⊢ ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
22	18 20 21	sniffsupp	⊢ ( 𝜑 → ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) finSupp 0 )
23	2 3 4 17 22	dprdwd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) ∈ 𝑊 )
24	7 23	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
25		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
26		dprdgrp	⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
27		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
28	3 26 27	3syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
29	2 3 4 24 25	dprdff	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
30	7	oveq1i	⊢ ( 𝐹 supp 0 ) = ( ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) supp 0 )
31		eldifsni	⊢ ( 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) → 𝑛 ≠ 𝑋 )
32	31	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → 𝑛 ≠ 𝑋 )
33		ifnefalse	⊢ ( 𝑛 ≠ 𝑋 → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 0 )
34	32 33	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 0 )
35	34 18	suppss2	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ⊆ { 𝑋 } )
36	30 35	eqsstrid	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ { 𝑋 } )
37	25 1 28 18 5 29 36	gsumpt	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐹 ‘ 𝑋 ) )
38		iftrue	⊢ ( 𝑛 = 𝑋 → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 𝐴 )
39	7 38 5 6	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝐴 )
40	37 39	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 𝐴 )
41	24 40	jca	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( 𝐺 Σg 𝐹 ) = 𝐴 ) )