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