MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldmdprd Unicode version

Theorem reldmdprd 15487
Description: The domain of definition of the internal direct product, which states that  S is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.)
Assertion
Ref Expression
reldmdprd  |-  Rel  dom DProd

Proof of Theorem reldmdprd
Dummy variables  g  h  f  s  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-dprd 15485 . 2  |- 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 " ( _V  \  {
( 0g `  g
) } ) )  e.  Fin }  |->  ( g  gsumg  f ) ) )
21reldmmpt2 6122 1  |-  Rel  dom DProd
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1649    e. wcel 1717   {cab 2375   A.wral 2651   {crab 2655   _Vcvv 2901    \ cdif 3262    i^i cin 3264    C_ wss 3265   {csn 3759   U.cuni 3959    e. cmpt 4209   `'ccnv 4819   dom cdm 4820   ran crn 4821   "cima 4823   Rel wrel 4825   -->wf 5392   ` cfv 5396  (class class class)co 6022   X_cixp 7001   Fincfn 7047   0gc0g 13652    gsumg cgsu 13653  mrClscmrc 13737   Grpcgrp 14614  SubGrpcsubg 14867  Cntzccntz 15043   DProd cdprd 15483
This theorem is referenced by:  dprdval  15490  dprdgrp  15492  dprdf  15493  dprdcntz  15495  dprddisj  15496  dprdw  15497  dprdssv  15503  dprdfid  15504  dprdfinv  15506  dprdfadd  15507  dprdfsub  15508  dprdfeq0  15509  dprdf11  15510  dprdlub  15513  dprdres  15515  dprdss  15516  dprdf1o  15519  subgdmdprd  15521  dmdprdsplitlem  15524  dprddisj2  15526  dprd2da  15529  dmdprdsplit2  15533  dpjfval  15542  dpjidcl  15545
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-br 4156  df-opab 4210  df-xp 4826  df-rel 4827  df-dm 4830  df-oprab 6026  df-mpt2 6027  df-dprd 15485
  Copyright terms: Public domain W3C validator