Metamath Proof Explorer

Theorem dprd2dlem1

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 ) )
dprd2d.6 
|- ( ph -> C C_ I )
Assertion dprd2dlem1 
|- ( ph -> ( K ` U. ( S " ( A |` C ) ) ) = ( G DProd ( i e. C |-> ( 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 dprd2d.6 
 |-  ( ph -> C C_ I )
8 dprdgrp 
 |-  ( G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) -> G e. Grp )
9 5 8 syl 
 |-  ( ph -> G e. Grp )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 10 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
12 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
13 9 11 12 3syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
14 ffun 
 |-  ( S : A --> ( SubGrp ` G ) -> Fun S )
15 funiunfv 
 |-  ( Fun S -> U_ x e. ( A |` C ) ( S ` x ) = U. ( S " ( A |` C ) ) )
16 2 14 15 3syl 
 |-  ( ph -> U_ x e. ( A |` C ) ( S ` x ) = U. ( S " ( A |` C ) ) )
17 resss 
 |-  ( A |` C ) C_ A
18 17 sseli 
 |-  ( x e. ( A |` C ) -> x e. A )
19 1 2 3 4 5 6 dprd2dlem2 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
20 18 19 sylan2 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> ( S ` x ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
21 1st2nd 
 |-  ( ( Rel A /\ x e. A ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
22 1 18 21 syl2an 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
23 simpr 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> x e. ( A |` C ) )
24 22 23 eqeltrrd 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` C ) )
25 fvex 
 |-  ( 2nd ` x ) e. _V
26 25 opelresi 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` C ) <-> ( ( 1st ` x ) e. C /\ <. ( 1st ` x ) , ( 2nd ` x ) >. e. A ) )
27 26 simplbi 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` C ) -> ( 1st ` x ) e. C )
28 24 27 syl 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> ( 1st ` x ) e. C )
29 ovex 
 |-  ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. _V
30 eqid 
 |-  ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) )
31 sneq 
 |-  ( i = ( 1st ` x ) -> { i } = { ( 1st ` x ) } )
32 31 imaeq2d 
 |-  ( i = ( 1st ` x ) -> ( A " { i } ) = ( A " { ( 1st ` x ) } ) )
33 oveq1 
 |-  ( i = ( 1st ` x ) -> ( i S j ) = ( ( 1st ` x ) S j ) )
34 32 33 mpteq12dv 
 |-  ( i = ( 1st ` x ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
35 34 oveq2d 
 |-  ( i = ( 1st ` x ) -> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
36 30 35 elrnmpt1s 
 |-  ( ( ( 1st ` x ) e. C /\ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. _V ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
37 28 29 36 sylancl 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
38 elssuni 
 |-  ( ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
39 37 38 syl 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
40 20 39 sstrd 
 |-  ( ( ph /\ x e. ( A |` C ) ) -> ( S ` x ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
41 40 ralrimiva 
 |-  ( ph -> A. x e. ( A |` C ) ( S ` x ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
42 iunss 
 |-  ( U_ x e. ( A |` C ) ( S ` x ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) <-> A. x e. ( A |` C ) ( S ` x ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
43 41 42 sylibr 
 |-  ( ph -> U_ x e. ( A |` C ) ( S ` x ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
44 16 43 eqsstrrd 
 |-  ( ph -> U. ( S " ( A |` C ) ) C_ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
45 7 sselda 
 |-  ( ( ph /\ i e. C ) -> i e. I )
46 45 4 syldan 
 |-  ( ( ph /\ i e. C ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
47 ovex 
 |-  ( i S j ) e. _V
48 eqid 
 |-  ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { i } ) |-> ( i S j ) )
49 47 48 dmmpti 
 |-  dom ( j e. ( A " { i } ) |-> ( i S j ) ) = ( A " { i } )
50 49 a1i 
 |-  ( ( ph /\ i e. C ) -> dom ( j e. ( A " { i } ) |-> ( i S j ) ) = ( A " { i } ) )
51 imassrn 
 |-  ( S " ( A |` C ) ) C_ ran S
52 2 frnd 
 |-  ( ph -> ran S C_ ( SubGrp ` G ) )
53 mresspw 
 |-  ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
54 13 53 syl 
 |-  ( ph -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
55 52 54 sstrd 
 |-  ( ph -> ran S C_ ~P ( Base ` G ) )
56 51 55 sstrid 
 |-  ( ph -> ( S " ( A |` C ) ) C_ ~P ( Base ` G ) )
57 sspwuni 
 |-  ( ( S " ( A |` C ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( A |` C ) ) C_ ( Base ` G ) )
58 56 57 sylib 
 |-  ( ph -> U. ( S " ( A |` C ) ) C_ ( Base ` G ) )
59 6 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( A |` C ) ) C_ ( Base ` G ) ) -> ( K ` U. ( S " ( A |` C ) ) ) e. ( SubGrp ` G ) )
60 13 58 59 syl2anc 
 |-  ( ph -> ( K ` U. ( S " ( A |` C ) ) ) e. ( SubGrp ` G ) )
61 60 adantr 
 |-  ( ( ph /\ i e. C ) -> ( K ` U. ( S " ( A |` C ) ) ) e. ( SubGrp ` G ) )
62 oveq2 
 |-  ( j = k -> ( i S j ) = ( i S k ) )
63 62 48 47 fvmpt3i 
 |-  ( k e. ( A " { i } ) -> ( ( j e. ( A " { i } ) |-> ( i S j ) ) ` k ) = ( i S k ) )
64 63 adantl 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> ( ( j e. ( A " { i } ) |-> ( i S j ) ) ` k ) = ( i S k ) )
65 df-ov 
 |-  ( i S k ) = ( S ` <. i , k >. )
66 2 ffnd 
 |-  ( ph -> S Fn A )
67 66 ad2antrr 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> S Fn A )
68 17 a1i 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> ( A |` C ) C_ A )
69 simplr 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> i e. C )
70 elrelimasn 
 |-  ( Rel A -> ( k e. ( A " { i } ) <-> i A k ) )
71 1 70 syl 
 |-  ( ph -> ( k e. ( A " { i } ) <-> i A k ) )
72 71 adantr 
 |-  ( ( ph /\ i e. C ) -> ( k e. ( A " { i } ) <-> i A k ) )
73 72 biimpa 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> i A k )
74 df-br 
 |-  ( i A k <-> <. i , k >. e. A )
75 73 74 sylib 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> <. i , k >. e. A )
76 vex 
 |-  k e. _V
77 76 opelresi 
 |-  ( <. i , k >. e. ( A |` C ) <-> ( i e. C /\ <. i , k >. e. A ) )
78 69 75 77 sylanbrc 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> <. i , k >. e. ( A |` C ) )
79 fnfvima 
 |-  ( ( S Fn A /\ ( A |` C ) C_ A /\ <. i , k >. e. ( A |` C ) ) -> ( S ` <. i , k >. ) e. ( S " ( A |` C ) ) )
80 67 68 78 79 syl3anc 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> ( S ` <. i , k >. ) e. ( S " ( A |` C ) ) )
81 65 80 eqeltrid 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> ( i S k ) e. ( S " ( A |` C ) ) )
82 elssuni 
 |-  ( ( i S k ) e. ( S " ( A |` C ) ) -> ( i S k ) C_ U. ( S " ( A |` C ) ) )
83 81 82 syl 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> ( i S k ) C_ U. ( S " ( A |` C ) ) )
84 13 6 58 mrcssidd 
 |-  ( ph -> U. ( S " ( A |` C ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
85 84 ad2antrr 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> U. ( S " ( A |` C ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
86 83 85 sstrd 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> ( i S k ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
87 64 86 eqsstrd 
 |-  ( ( ( ph /\ i e. C ) /\ k e. ( A " { i } ) ) -> ( ( j e. ( A " { i } ) |-> ( i S j ) ) ` k ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
88 46 50 61 87 dprdlub 
 |-  ( ( ph /\ i e. C ) -> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
89 ovex 
 |-  ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) e. _V
90 89 elpw 
 |-  ( ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) e. ~P ( K ` U. ( S " ( A |` C ) ) ) <-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
91 88 90 sylibr 
 |-  ( ( ph /\ i e. C ) -> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) e. ~P ( K ` U. ( S " ( A |` C ) ) ) )
92 91 fmpttd 
 |-  ( ph -> ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) : C --> ~P ( K ` U. ( S " ( A |` C ) ) ) )
93 92 frnd 
 |-  ( ph -> ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) C_ ~P ( K ` U. ( S " ( A |` C ) ) ) )
94 sspwuni 
 |-  ( ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) C_ ~P ( K ` U. ( S " ( A |` C ) ) ) <-> U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
95 93 94 sylib 
 |-  ( ph -> U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
96 13 6 mrcssvd 
 |-  ( ph -> ( K ` U. ( S " ( A |` C ) ) ) C_ ( Base ` G ) )
97 95 96 sstrd 
 |-  ( ph -> U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) C_ ( Base ` G ) )
98 13 6 44 97 mrcssd 
 |-  ( ph -> ( K ` U. ( S " ( A |` C ) ) ) C_ ( K ` U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
99 6 mrcsscl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) /\ ( K ` U. ( S " ( A |` C ) ) ) e. ( SubGrp ` G ) ) -> ( K ` U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
100 13 95 60 99 syl3anc 
 |-  ( ph -> ( K ` U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) C_ ( K ` U. ( S " ( A |` C ) ) ) )
101 98 100 eqssd 
 |-  ( ph -> ( K ` U. ( S " ( A |` C ) ) ) = ( K ` U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
102 eqid 
 |-  ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) )
103 89 102 dmmpti 
 |-  dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = I
104 103 a1i 
 |-  ( ph -> dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = I )
105 5 104 7 dprdres 
 |-  ( ph -> ( G dom DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` C ) /\ ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` C ) ) C_ ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) ) )
106 105 simpld 
 |-  ( ph -> G dom DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` C ) )
107 7 resmptd 
 |-  ( ph -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` C ) = ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
108 106 107 breqtrd 
 |-  ( ph -> G dom DProd ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
109 6 dprdspan 
 |-  ( G dom DProd ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) -> ( G DProd ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) = ( K ` U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
110 108 109 syl 
 |-  ( ph -> ( G DProd ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) = ( K ` U. ran ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
111 101 110 eqtr4d 
 |-  ( ph -> ( K ` U. ( S " ( A |` C ) ) ) = ( G DProd ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )