This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ dom ⁡ S = I → A ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ W A = ∑ G f