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 = ( 0g ‘ 𝐺 )
	dprdval.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
Assertion	eldprd	⊢ ( dom 𝑆 = 𝐼 → ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dprdval.0	⊢ 0 = ( 0g ‘ 𝐺 )
2		dprdval.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
3		elfvdm	⊢ ( 𝐴 ∈ ( DProd ‘ ⟨ 𝐺 , 𝑆 ⟩ ) → ⟨ 𝐺 , 𝑆 ⟩ ∈ dom DProd )
4		df-ov	⊢ ( 𝐺 DProd 𝑆 ) = ( DProd ‘ ⟨ 𝐺 , 𝑆 ⟩ )
5	3 4	eleq2s	⊢ ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) → ⟨ 𝐺 , 𝑆 ⟩ ∈ dom DProd )
6		df-br	⊢ ( 𝐺 dom DProd 𝑆 ↔ ⟨ 𝐺 , 𝑆 ⟩ ∈ dom DProd )
7	5 6	sylibr	⊢ ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) → 𝐺 dom DProd 𝑆 )
8	7	pm4.71ri	⊢ ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ) )
9	1 2	dprdval	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) )
10	9	eleq2d	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ 𝐴 ∈ ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) ) )
11		eqid	⊢ ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) = ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) )
12		ovex	⊢ ( 𝐺 Σg 𝑓 ) ∈ V
13	11 12	elrnmpti	⊢ ( 𝐴 ∈ ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) ↔ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) )
14	10 13	bitrdi	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) )
15	14	ancoms	⊢ ( ( dom 𝑆 = 𝐼 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) )
16	15	pm5.32da	⊢ ( dom 𝑆 = 𝐼 → ( ( 𝐺 dom DProd 𝑆 ∧ 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) )
17	8 16	syl5bb	⊢ ( dom 𝑆 = 𝐼 → ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) )