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	⊢ 𝑊 = { ℎ ∈ 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 = ( 0_g ‘ 𝐺 )
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 𝑆 ) )