This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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