Metamath Proof Explorer

Theorem dprd2dlem2

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-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 dprd2dlem2 
|- ( ( ph /\ X e. A ) -> ( S ` X ) C_ ( G DProd ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) 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 df-ov 
 |-  ( ( 1st ` X ) S ( 2nd ` X ) ) = ( S ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
8 1st2nd 
 |-  ( ( Rel A /\ X e. A ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
9 1 8 sylan 
 |-  ( ( ph /\ X e. A ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
10 simpr 
 |-  ( ( ph /\ X e. A ) -> X e. A )
11 9 10 eqeltrrd 
 |-  ( ( ph /\ X e. A ) -> <. ( 1st ` X ) , ( 2nd ` X ) >. e. A )
12 df-br 
 |-  ( ( 1st ` X ) A ( 2nd ` X ) <-> <. ( 1st ` X ) , ( 2nd ` X ) >. e. A )
13 11 12 sylibr 
 |-  ( ( ph /\ X e. A ) -> ( 1st ` X ) A ( 2nd ` X ) )
14 1 adantr 
 |-  ( ( ph /\ X e. A ) -> Rel A )
15 elrelimasn 
 |-  ( Rel A -> ( ( 2nd ` X ) e. ( A " { ( 1st ` X ) } ) <-> ( 1st ` X ) A ( 2nd ` X ) ) )
16 14 15 syl 
 |-  ( ( ph /\ X e. A ) -> ( ( 2nd ` X ) e. ( A " { ( 1st ` X ) } ) <-> ( 1st ` X ) A ( 2nd ` X ) ) )
17 13 16 mpbird 
 |-  ( ( ph /\ X e. A ) -> ( 2nd ` X ) e. ( A " { ( 1st ` X ) } ) )
18 oveq2 
 |-  ( j = ( 2nd ` X ) -> ( ( 1st ` X ) S j ) = ( ( 1st ` X ) S ( 2nd ` X ) ) )
19 eqid 
 |-  ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) = ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) )
20 ovex 
 |-  ( ( 1st ` X ) S j ) e. _V
21 18 19 20 fvmpt3i 
 |-  ( ( 2nd ` X ) e. ( A " { ( 1st ` X ) } ) -> ( ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ` ( 2nd ` X ) ) = ( ( 1st ` X ) S ( 2nd ` X ) ) )
22 17 21 syl 
 |-  ( ( ph /\ X e. A ) -> ( ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ` ( 2nd ` X ) ) = ( ( 1st ` X ) S ( 2nd ` X ) ) )
23 9 fveq2d 
 |-  ( ( ph /\ X e. A ) -> ( S ` X ) = ( S ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
24 7 22 23 3eqtr4a 
 |-  ( ( ph /\ X e. A ) -> ( ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ` ( 2nd ` X ) ) = ( S ` X ) )
25 sneq 
 |-  ( i = ( 1st ` X ) -> { i } = { ( 1st ` X ) } )
26 25 imaeq2d 
 |-  ( i = ( 1st ` X ) -> ( A " { i } ) = ( A " { ( 1st ` X ) } ) )
27 oveq1 
 |-  ( i = ( 1st ` X ) -> ( i S j ) = ( ( 1st ` X ) S j ) )
28 26 27 mpteq12dv 
 |-  ( i = ( 1st ` X ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) )
29 28 breq2d 
 |-  ( i = ( 1st ` X ) -> ( G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) <-> G dom DProd ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ) )
30 4 ralrimiva 
 |-  ( ph -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
31 30 adantr 
 |-  ( ( ph /\ X e. A ) -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
32 3 adantr 
 |-  ( ( ph /\ X e. A ) -> dom A C_ I )
33 1stdm 
 |-  ( ( Rel A /\ X e. A ) -> ( 1st ` X ) e. dom A )
34 1 33 sylan 
 |-  ( ( ph /\ X e. A ) -> ( 1st ` X ) e. dom A )
35 32 34 sseldd 
 |-  ( ( ph /\ X e. A ) -> ( 1st ` X ) e. I )
36 29 31 35 rspcdva 
 |-  ( ( ph /\ X e. A ) -> G dom DProd ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) )
37 20 19 dmmpti 
 |-  dom ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) = ( A " { ( 1st ` X ) } )
38 37 a1i 
 |-  ( ( ph /\ X e. A ) -> dom ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) = ( A " { ( 1st ` X ) } ) )
39 36 38 17 dprdub 
 |-  ( ( ph /\ X e. A ) -> ( ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ` ( 2nd ` X ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ) )
40 24 39 eqsstrrd 
 |-  ( ( ph /\ X e. A ) -> ( S ` X ) C_ ( G DProd ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ) )