Metamath Proof Explorer


Theorem dprdf

Description: The function S is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdf GdomDProdSS:domSSubGrpG

Proof

Step Hyp Ref Expression
1 reldmdprd ReldomDProd
2 1 brrelex2i GdomDProdSSV
3 2 dmexd GdomDProdSdomSV
4 eqid domS=domS
5 eqid CntzG=CntzG
6 eqid 0G=0G
7 eqid mrClsSubGrpG=mrClsSubGrpG
8 5 6 7 dmdprd domSVdomS=domSGdomDProdSGGrpS:domSSubGrpGxdomSydomSxSxCntzGSySxmrClsSubGrpGSdomSx=0G
9 3 4 8 sylancl GdomDProdSGdomDProdSGGrpS:domSSubGrpGxdomSydomSxSxCntzGSySxmrClsSubGrpGSdomSx=0G
10 9 ibi GdomDProdSGGrpS:domSSubGrpGxdomSydomSxSxCntzGSySxmrClsSubGrpGSdomSx=0G
11 10 simp2d GdomDProdSS:domSSubGrpG