Metamath Proof Explorer


Theorem dprd2db

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprd2d.1 φRelA
dprd2d.2 φS:ASubGrpG
dprd2d.3 φdomAI
dprd2d.4 φiIGdomDProdjAiiSj
dprd2d.5 φGdomDProdiIGDProdjAiiSj
dprd2d.k K=mrClsSubGrpG
Assertion dprd2db φGDProdS=GDProdiIGDProdjAiiSj

Proof

Step Hyp Ref Expression
1 dprd2d.1 φRelA
2 dprd2d.2 φS:ASubGrpG
3 dprd2d.3 φdomAI
4 dprd2d.4 φiIGdomDProdjAiiSj
5 dprd2d.5 φGdomDProdiIGDProdjAiiSj
6 dprd2d.k K=mrClsSubGrpG
7 1 2 3 4 5 6 dprd2da φGdomDProdS
8 6 dprdspan GdomDProdSGDProdS=KranS
9 7 8 syl φGDProdS=KranS
10 relssres RelAdomAIAI=A
11 1 3 10 syl2anc φAI=A
12 11 imaeq2d φSAI=SA
13 ffn S:ASubGrpGSFnA
14 fnima SFnASA=ranS
15 2 13 14 3syl φSA=ranS
16 12 15 eqtr2d φranS=SAI
17 16 unieqd φranS=SAI
18 17 fveq2d φKranS=KSAI
19 ssidd φII
20 1 2 3 4 5 6 19 dprd2dlem1 φKSAI=GDProdiIGDProdjAiiSj
21 9 18 20 3eqtrd φGDProdS=GDProdiIGDProdjAiiSj