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

Metamath Proof Explorer

Theorem eldprdi

Description: The domain of definition of the internal direct product, which states that S is a family of subgroups that mutually commute and have trivial intersections. (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
eldprdi.3 ⊢ φ → F ∈ W
Assertion eldprdi ⊢ φ → ∑ G F ∈ G DProd S

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 eldprdi.3 ⊢ φ → F ∈ W
6 eqid ⊢ ∑ G F = ∑ G F
7 oveq2 ⊢ f = F → ∑ G f = ∑ G F
8 7 rspceeqv ⊢ F ∈ W ∧ ∑ G F = ∑ G F → ∃ f ∈ W ∑ G F = ∑ G f
9 5 6 8 sylancl ⊢ φ → ∃ f ∈ W ∑ G F = ∑ G f
10 1 2 eldprd ⊢ dom ⁡ S = I → ∑ G F ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ W ∑ G F = ∑ G f
11 4 10 syl ⊢ φ → ∑ G F ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ W ∑ G F = ∑ G f
12 3 9 11 mpbir2and ⊢ φ → ∑ G F ∈ G DProd S