Theorem dprd0

Description: The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypothesis	dprd0.0	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	dprd0	⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		dprd0.0	⊢ 0 = ( 0g ‘ 𝐺 )
2		0ex	⊢ ∅ ∈ V
3	1	dprdz	⊢ ( ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) )
4	2 3	mpan2	⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) )
5		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ { 0 } ) = ∅
6	5	breq2i	⊢ ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ↔ 𝐺 dom DProd ∅ )
7	5	oveq2i	⊢ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = ( 𝐺 DProd ∅ )
8	7	eqeq1i	⊢ ( ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ↔ ( 𝐺 DProd ∅ ) = { 0 } )
9	6 8	anbi12i	⊢ ( ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) ↔ ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )
10	4 9	sylib	⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )