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
|- ( ph -> Rel A )
dprd2d.2
|- ( ph -> S : A --> ( SubGrp ` G ) )
dprd2d.3
|- ( ph -> dom A C_ I )
dprd2d.4
|- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
dprd2d.5
|- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
dprd2d.k
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion dprd2db
|- ( ph -> ( G DProd S ) = ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dprd2d.1
 |-  ( ph -> Rel A )
2 dprd2d.2
 |-  ( ph -> S : A --> ( SubGrp ` G ) )
3 dprd2d.3
 |-  ( ph -> dom A C_ I )
4 dprd2d.4
 |-  ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
5 dprd2d.5
 |-  ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
6 dprd2d.k
 |-  K = ( mrCls ` ( SubGrp ` G ) )
7 1 2 3 4 5 6 dprd2da
 |-  ( ph -> G dom DProd S )
8 6 dprdspan
 |-  ( G dom DProd S -> ( G DProd S ) = ( K ` U. ran S ) )
9 7 8 syl
 |-  ( ph -> ( G DProd S ) = ( K ` U. ran S ) )
10 relssres
 |-  ( ( Rel A /\ dom A C_ I ) -> ( A |` I ) = A )
11 1 3 10 syl2anc
 |-  ( ph -> ( A |` I ) = A )
12 11 imaeq2d
 |-  ( ph -> ( S " ( A |` I ) ) = ( S " A ) )
13 ffn
 |-  ( S : A --> ( SubGrp ` G ) -> S Fn A )
14 fnima
 |-  ( S Fn A -> ( S " A ) = ran S )
15 2 13 14 3syl
 |-  ( ph -> ( S " A ) = ran S )
16 12 15 eqtr2d
 |-  ( ph -> ran S = ( S " ( A |` I ) ) )
17 16 unieqd
 |-  ( ph -> U. ran S = U. ( S " ( A |` I ) ) )
18 17 fveq2d
 |-  ( ph -> ( K ` U. ran S ) = ( K ` U. ( S " ( A |` I ) ) ) )
19 ssidd
 |-  ( ph -> I C_ I )
20 1 2 3 4 5 6 19 dprd2dlem1
 |-  ( ph -> ( K ` U. ( S " ( A |` I ) ) ) = ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
21 9 18 20 3eqtrd
 |-  ( ph -> ( G DProd S ) = ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )