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 ` G )
Assertion	dprd0	|- ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		dprd0.0	|- .0. = ( 0g ` G )
2		0ex	|- (/) e. _V
3	1	dprdz	|- ( ( G e. Grp /\ (/) e. _V ) -> ( G dom DProd ( x e. (/) |-> { .0. } ) /\ ( G DProd ( x e. (/) |-> { .0. } ) ) = { .0. } ) )
4	2 3	mpan2	|- ( G e. Grp -> ( G dom DProd ( x e. (/) |-> { .0. } ) /\ ( G DProd ( x e. (/) |-> { .0. } ) ) = { .0. } ) )
5		mpt0	|- ( x e. (/) |-> { .0. } ) = (/)
6	5	breq2i	|- ( G dom DProd ( x e. (/) |-> { .0. } ) <-> G dom DProd (/) )
7	5	oveq2i	|- ( G DProd ( x e. (/) |-> { .0. } ) ) = ( G DProd (/) )
8	7	eqeq1i	|- ( ( G DProd ( x e. (/) |-> { .0. } ) ) = { .0. } <-> ( G DProd (/) ) = { .0. } )
9	6 8	anbi12i	|- ( ( G dom DProd ( x e. (/) |-> { .0. } ) /\ ( G DProd ( x e. (/) |-> { .0. } ) ) = { .0. } ) <-> ( G dom DProd (/) /\ ( G DProd (/) ) = { .0. } ) )
10	4 9	sylib	|- ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { .0. } ) )