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 = ( 0g ‘ 𝐺 )
	eldprdi.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
	eldprdi.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	eldprdi.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	eldprdi.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
Assertion	eldprdi	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) )

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		eqid	⊢ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 )
7		oveq2	⊢ ( 𝑓 = 𝐹 → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg 𝐹 ) )
8	7	rspceeqv	⊢ ( ( 𝐹 ∈ 𝑊 ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) ) → ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
9	5 6 8	sylancl	⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
10	1 2	eldprd	⊢ ( dom 𝑆 = 𝐼 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
11	4 10	syl	⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
12	3 9 11	mpbir2and	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) )