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

Theorem reldmdprd 15548
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 15546 . 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 6173 1  |-  Rel  dom DProd
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1652    e. wcel 1725   {cab 2421   A.wral 2697   {crab 2701   _Vcvv 2948    \ cdif 3309    i^i cin 3311    C_ wss 3312   {csn 3806   U.cuni 4007    e. cmpt 4258   `'ccnv 4869   dom cdm 4870   ran crn 4871   "cima 4873   Rel wrel 4875   -->wf 5442   ` cfv 5446  (class class class)co 6073   X_cixp 7055   Fincfn 7101   0gc0g 13713    gsumg cgsu 13714  mrClscmrc 13798   Grpcgrp 14675  SubGrpcsubg 14928  Cntzccntz 15104   DProd cdprd 15544
This theorem is referenced by:  dprdval  15551  dprdgrp  15553  dprdf  15554  dprdcntz  15556  dprddisj  15557  dprdw  15558  dprdssv  15564  dprdfid  15565  dprdfinv  15567  dprdfadd  15568  dprdfsub  15569  dprdfeq0  15570  dprdf11  15571  dprdlub  15574  dprdres  15576  dprdss  15577  dprdf1o  15580  subgdmdprd  15582  dmdprdsplitlem  15585  dprddisj2  15587  dprd2da  15590  dmdprdsplit2  15594  dpjfval  15603  dpjidcl  15606
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-xp 4876  df-rel 4877  df-dm 4880  df-oprab 6077  df-mpt2 6078  df-dprd 15546
  Copyright terms: Public domain W3C validator