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 = ( 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 ffvelrnda ( ( 𝜑𝑛𝐼 ) → ( 𝑆𝑛 ) ∈ ( 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 𝐹 ) = 𝐴 ) )