Metamath Proof Explorer

Theorem dprdf11

Description: Two group sums over a direct product that give the same value are equal as functions. (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 ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
dprdf11.4 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
Assertion dprdf11 ( 𝜑 → ( ( 𝐺 Σ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 dprdf11.4 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 2 3 4 5 7 dprdff ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
9 8 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
10 2 3 4 6 7 dprdff ⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
11 10 ffnd ⊢ ( 𝜑 → 𝐻 Fn 𝐼 )
12 eqfnfv ⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝐻 Fn 𝐼 ) → ( 𝐹 = 𝐻 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
13 9 11 12 syl2anc ⊢ ( 𝜑 → ( 𝐹 = 𝐻 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
14 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
15 1 2 3 4 5 6 14 dprdfsub ⊢ ( 𝜑 → ( ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝐻 ) ) ) )
16 15 simpld ⊢ ( 𝜑 → ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) ∈ 𝑊 )
17 1 2 3 4 16 dprdfeq0 ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) ) = 0 ↔ ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) ) )
18 15 simprd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝐻 ) ) )
19 18 eqeq1d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) ) = 0 ↔ ( ( 𝐺 Σg 𝐹 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝐻 ) ) = 0 ) )
20 3 4 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
21 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
22 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑥 ) ∈ V )
23 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
24 10 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐻 ‘ 𝑥 ) ) )
25 20 21 22 23 24 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ) )
26 25 eqeq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) ↔ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) ) )
27 ovex ⊢ ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ∈ V
28 27 rgenw ⊢ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ∈ V
29 mpteqb ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) = 0 ) )
30 28 29 ax-mp ⊢ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) = 0 )
31 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
32 3 31 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ Grp )
34 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
35 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
36 7 1 14 grpsubeq0 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐻 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
37 33 34 35 36 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) = 0 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
38 37 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) = 0 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
39 30 38 syl5bb ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
40 26 39 bitrd ⊢ ( 𝜑 → ( ( 𝐹 ∘f ( -g ‘ 𝐺 ) 𝐻 ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
41 17 19 40 3bitr3d ⊢ ( 𝜑 → ( ( ( 𝐺 Σg 𝐹 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝐻 ) ) = 0 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) ) )
42 7 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 7 1 14 grpsubeq0 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐺 Σg 𝐹 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐺 Σg 𝐻 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 𝐺 Σg 𝐹 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝐻 ) ) = 0 ↔ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) ) )
48 32 44 46 47 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐺 Σg 𝐹 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝐻 ) ) = 0 ↔ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) ) )
49 13 41 48 3bitr2rd ⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐻 ) ↔ 𝐹 = 𝐻 ) )