Description: The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016) (Proof shortened by AV, 11-Jul-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | reldmdprd | |- Rel dom DProd |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-dprd | |- DProd = ( g e. Grp , s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } |-> ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) ) |
|
| 2 | 1 | reldmmpo | |- Rel dom DProd |