Metamath Proof Explorer


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. } ) )