Metamath Proof Explorer

Theorem eldprd

Description: A class A is an internal direct product iff it is the (group) sum of an infinite, but finitely supported cartesian product of subgroups (which mutually commute and have trivial intersections). (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Hypotheses dprdval.0 ⊢ 0 ˙ = 0 G
dprdval.w ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
Assertion eldprd ⊢ dom ⁡ S = I → A ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ W A = ∑ G f

Proof

Step Hyp Ref Expression
1 dprdval.0 ⊢ 0 ˙ = 0 G
2 dprdval.w ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
3 elfvdm ⊢ A ∈ DProd ⁡ G S → G S ∈ dom ⁡ DProd
4 df-ov ⊢ G DProd S = DProd ⁡ G S
5 3 4 eleq2s ⊢ A ∈ G DProd S → G S ∈ dom ⁡ DProd
6 df-br ⊢ G dom ⁡ DProd S ↔ G S ∈ dom ⁡ DProd
7 5 6 sylibr ⊢ A ∈ G DProd S → G dom ⁡ DProd S
8 7 pm4.71ri ⊢ A ∈ G DProd S ↔ G dom ⁡ DProd S ∧ A ∈ G DProd S
9 1 2 dprdval ⊢ G dom ⁡ DProd S ∧ dom ⁡ S = I → G DProd S = ran ⁡ f ∈ W ⟼ ∑ G f
10 9 eleq2d ⊢ G dom ⁡ DProd S ∧ dom ⁡ S = I → A ∈ G DProd S ↔ A ∈ ran ⁡ f ∈ W ⟼ ∑ G f
11 eqid ⊢ f ∈ W ⟼ ∑ G f = f ∈ W ⟼ ∑ G f
12 ovex ⊢ ∑ G f ∈ V
13 11 12 elrnmpti ⊢ A ∈ ran ⁡ f ∈ W ⟼ ∑ G f ↔ ∃ f ∈ W A = ∑ G f
14 10 13 bitrdi ⊢ G dom ⁡ DProd S ∧ dom ⁡ S = I → A ∈ G DProd S ↔ ∃ f ∈ W A = ∑ G f
15 14 ancoms ⊢ dom ⁡ S = I ∧ G dom ⁡ DProd S → A ∈ G DProd S ↔ ∃ f ∈ W A = ∑ G f
16 15 pm5.32da ⊢ dom ⁡ S = I → G dom ⁡ DProd S ∧ A ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ W A = ∑ G f
17 8 16 syl5bb ⊢ dom ⁡ S = I → A ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ W A = ∑ G f