Metamath Proof Explorer


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 ˙ = 0 G
eldprdi.w W = h i I S i | finSupp 0 ˙ h
eldprdi.1 φ G dom DProd S
eldprdi.2 φ dom S = I
dprdfid.3 φ X I
dprdfid.4 φ A S X
dprdfid.f F = n I if n = X A 0 ˙
Assertion dprdfid φ F W G F = A

Proof

Step Hyp Ref Expression
1 eldprdi.0 0 ˙ = 0 G
2 eldprdi.w W = h i I S i | finSupp 0 ˙ h
3 eldprdi.1 φ G dom DProd S
4 eldprdi.2 φ dom S = I
5 dprdfid.3 φ X I
6 dprdfid.4 φ A S X
7 dprdfid.f F = n I if n = X A 0 ˙
8 6 ad2antrr φ n I n = X A S X
9 simpr φ n I n = X n = X
10 9 fveq2d φ n I n = X S n = S X
11 8 10 eleqtrrd φ n I n = X A S n
12 3 4 dprdf2 φ S : I SubGrp G
13 12 ffvelrnda φ n I S n SubGrp G
14 1 subg0cl S n SubGrp G 0 ˙ S n
15 13 14 syl φ n I 0 ˙ S n
16 15 adantr φ n I ¬ n = X 0 ˙ S n
17 11 16 ifclda φ n I if n = X A 0 ˙ S n
18 3 4 dprddomcld φ I V
19 1 fvexi 0 ˙ V
20 19 a1i φ 0 ˙ V
21 eqid n I if n = X A 0 ˙ = n I if n = X A 0 ˙
22 18 20 21 sniffsupp φ finSupp 0 ˙ n I if n = X A 0 ˙
23 2 3 4 17 22 dprdwd φ n I if n = X A 0 ˙ W
24 7 23 eqeltrid φ F W
25 eqid Base G = Base G
26 dprdgrp G dom DProd S G Grp
27 grpmnd G Grp G Mnd
28 3 26 27 3syl φ G Mnd
29 2 3 4 24 25 dprdff φ F : I Base G
30 7 oveq1i F supp 0 ˙ = n I if n = X A 0 ˙ supp 0 ˙
31 eldifsni n I X n X
32 31 adantl φ n I X n X
33 ifnefalse n X if n = X A 0 ˙ = 0 ˙
34 32 33 syl φ n I X if n = X A 0 ˙ = 0 ˙
35 34 18 suppss2 φ n I if n = X A 0 ˙ supp 0 ˙ X
36 30 35 eqsstrid φ F supp 0 ˙ X
37 25 1 28 18 5 29 36 gsumpt φ G F = F X
38 iftrue n = X if n = X A 0 ˙ = A
39 7 38 5 6 fvmptd3 φ F X = A
40 37 39 eqtrd φ G F = A
41 24 40 jca φ F W G F = A