Metamath Proof Explorer

Theorem dprd2d2

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

Ref Expression
Hypotheses dprd2d2.1 
|- ( ( ph /\ ( i e. I /\ j e. J ) ) -> S e. ( SubGrp ` G ) )
dprd2d2.2 
|- ( ( ph /\ i e. I ) -> G dom DProd ( j e. J |-> S ) )
dprd2d2.3 
|- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) )
Assertion dprd2d2 
|- ( ph -> ( G dom DProd ( i e. I , j e. J |-> S ) /\ ( G DProd ( i e. I , j e. J |-> S ) ) = ( G DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dprd2d2.1 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> S e. ( SubGrp ` G ) )
2 dprd2d2.2 
 |-  ( ( ph /\ i e. I ) -> G dom DProd ( j e. J |-> S ) )
3 dprd2d2.3 
 |-  ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) )
4 relxp 
 |-  Rel ( { i } X. J )
5 4 rgenw 
 |-  A. i e. I Rel ( { i } X. J )
6 reliun 
 |-  ( Rel U_ i e. I ( { i } X. J ) <-> A. i e. I Rel ( { i } X. J ) )
7 5 6 mpbir 
 |-  Rel U_ i e. I ( { i } X. J )
8 7 a1i 
 |-  ( ph -> Rel U_ i e. I ( { i } X. J ) )
9 1 ralrimivva 
 |-  ( ph -> A. i e. I A. j e. J S e. ( SubGrp ` G ) )
10 eqid 
 |-  ( i e. I , j e. J |-> S ) = ( i e. I , j e. J |-> S )
11 10 fmpox 
 |-  ( A. i e. I A. j e. J S e. ( SubGrp ` G ) <-> ( i e. I , j e. J |-> S ) : U_ i e. I ( { i } X. J ) --> ( SubGrp ` G ) )
12 9 11 sylib 
 |-  ( ph -> ( i e. I , j e. J |-> S ) : U_ i e. I ( { i } X. J ) --> ( SubGrp ` G ) )
13 dmiun 
 |-  dom U_ i e. I ( { i } X. J ) = U_ i e. I dom ( { i } X. J )
14 dmxpss 
 |-  dom ( { i } X. J ) C_ { i }
15 simpr 
 |-  ( ( ph /\ i e. I ) -> i e. I )
16 15 snssd 
 |-  ( ( ph /\ i e. I ) -> { i } C_ I )
17 14 16 sstrid 
 |-  ( ( ph /\ i e. I ) -> dom ( { i } X. J ) C_ I )
18 17 ralrimiva 
 |-  ( ph -> A. i e. I dom ( { i } X. J ) C_ I )
19 iunss 
 |-  ( U_ i e. I dom ( { i } X. J ) C_ I <-> A. i e. I dom ( { i } X. J ) C_ I )
20 18 19 sylibr 
 |-  ( ph -> U_ i e. I dom ( { i } X. J ) C_ I )
21 13 20 eqsstrid 
 |-  ( ph -> dom U_ i e. I ( { i } X. J ) C_ I )
22 simprl 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> i e. I )
23 simprr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> j e. J )
24 10 ovmpt4g 
 |-  ( ( i e. I /\ j e. J /\ S e. ( SubGrp ` G ) ) -> ( i ( i e. I , j e. J |-> S ) j ) = S )
25 22 23 1 24 syl3anc 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( i ( i e. I , j e. J |-> S ) j ) = S )
26 25 anassrs 
 |-  ( ( ( ph /\ i e. I ) /\ j e. J ) -> ( i ( i e. I , j e. J |-> S ) j ) = S )
27 26 mpteq2dva 
 |-  ( ( ph /\ i e. I ) -> ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) = ( j e. J |-> S ) )
28 2 27 breqtrrd 
 |-  ( ( ph /\ i e. I ) -> G dom DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) )
29 28 ralrimiva 
 |-  ( ph -> A. i e. I G dom DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) )
30 nfcv 
 |-  F/_ i G
31 nfcv 
 |-  F/_ i dom DProd
32 nfcsb1v 
 |-  F/_ i [_ x / i ]_ J
33 nfcv 
 |-  F/_ i x
34 nfmpo1 
 |-  F/_ i ( i e. I , j e. J |-> S )
35 nfcv 
 |-  F/_ i j
36 33 34 35 nfov 
 |-  F/_ i ( x ( i e. I , j e. J |-> S ) j )
37 32 36 nfmpt 
 |-  F/_ i ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) )
38 30 31 37 nfbr 
 |-  F/ i G dom DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) )
39 csbeq1a 
 |-  ( i = x -> J = [_ x / i ]_ J )
40 oveq1 
 |-  ( i = x -> ( i ( i e. I , j e. J |-> S ) j ) = ( x ( i e. I , j e. J |-> S ) j ) )
41 39 40 mpteq12dv 
 |-  ( i = x -> ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) = ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) )
42 41 breq2d 
 |-  ( i = x -> ( G dom DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) <-> G dom DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) ) )
43 38 42 rspc 
 |-  ( x e. I -> ( A. i e. I G dom DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) -> G dom DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) ) )
44 29 43 mpan9 
 |-  ( ( ph /\ x e. I ) -> G dom DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) )
45 nfcv 
 |-  F/_ y ( x ( i e. I , j e. J |-> S ) j )
46 nfcv 
 |-  F/_ j x
47 nfmpo2 
 |-  F/_ j ( i e. I , j e. J |-> S )
48 nfcv 
 |-  F/_ j y
49 46 47 48 nfov 
 |-  F/_ j ( x ( i e. I , j e. J |-> S ) y )
50 oveq2 
 |-  ( j = y -> ( x ( i e. I , j e. J |-> S ) j ) = ( x ( i e. I , j e. J |-> S ) y ) )
51 45 49 50 cbvmpt 
 |-  ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) = ( y e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) y ) )
52 nfv 
 |-  F/ i j = z
53 32 nfcri 
 |-  F/ i j e. [_ x / i ]_ J
54 52 53 nfan 
 |-  F/ i ( j = z /\ j e. [_ x / i ]_ J )
55 39 eleq2d 
 |-  ( i = x -> ( j e. J <-> j e. [_ x / i ]_ J ) )
56 55 anbi2d 
 |-  ( i = x -> ( ( j = z /\ j e. J ) <-> ( j = z /\ j e. [_ x / i ]_ J ) ) )
57 54 56 equsexv 
 |-  ( E. i ( i = x /\ ( j = z /\ j e. J ) ) <-> ( j = z /\ j e. [_ x / i ]_ J ) )
58 simprl 
 |-  ( ( ( ph /\ x e. I ) /\ ( i = x /\ j = z ) ) -> i = x )
59 simplr 
 |-  ( ( ( ph /\ x e. I ) /\ ( i = x /\ j = z ) ) -> x e. I )
60 58 59 eqeltrd 
 |-  ( ( ( ph /\ x e. I ) /\ ( i = x /\ j = z ) ) -> i e. I )
61 60 biantrurd 
 |-  ( ( ( ph /\ x e. I ) /\ ( i = x /\ j = z ) ) -> ( j e. J <-> ( i e. I /\ j e. J ) ) )
62 61 pm5.32da 
 |-  ( ( ph /\ x e. I ) -> ( ( ( i = x /\ j = z ) /\ j e. J ) <-> ( ( i = x /\ j = z ) /\ ( i e. I /\ j e. J ) ) ) )
63 anass 
 |-  ( ( ( i = x /\ j = z ) /\ j e. J ) <-> ( i = x /\ ( j = z /\ j e. J ) ) )
64 eqcom 
 |-  ( <. x , z >. = <. i , j >. <-> <. i , j >. = <. x , z >. )
65 vex 
 |-  i e. _V
66 vex 
 |-  j e. _V
67 65 66 opth 
 |-  ( <. i , j >. = <. x , z >. <-> ( i = x /\ j = z ) )
68 64 67 bitr2i 
 |-  ( ( i = x /\ j = z ) <-> <. x , z >. = <. i , j >. )
69 68 anbi1i 
 |-  ( ( ( i = x /\ j = z ) /\ ( i e. I /\ j e. J ) ) <-> ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) )
70 62 63 69 3bitr3g 
 |-  ( ( ph /\ x e. I ) -> ( ( i = x /\ ( j = z /\ j e. J ) ) <-> ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) ) )
71 70 exbidv 
 |-  ( ( ph /\ x e. I ) -> ( E. i ( i = x /\ ( j = z /\ j e. J ) ) <-> E. i ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) ) )
72 57 71 bitr3id 
 |-  ( ( ph /\ x e. I ) -> ( ( j = z /\ j e. [_ x / i ]_ J ) <-> E. i ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) ) )
73 72 exbidv 
 |-  ( ( ph /\ x e. I ) -> ( E. j ( j = z /\ j e. [_ x / i ]_ J ) <-> E. j E. i ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) ) )
74 vex 
 |-  z e. _V
75 eleq1w 
 |-  ( j = z -> ( j e. [_ x / i ]_ J <-> z e. [_ x / i ]_ J ) )
76 74 75 ceqsexv 
 |-  ( E. j ( j = z /\ j e. [_ x / i ]_ J ) <-> z e. [_ x / i ]_ J )
77 excom 
 |-  ( E. j E. i ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) <-> E. i E. j ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) )
78 73 76 77 3bitr3g 
 |-  ( ( ph /\ x e. I ) -> ( z e. [_ x / i ]_ J <-> E. i E. j ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) ) )
79 elrelimasn 
 |-  ( Rel U_ i e. I ( { i } X. J ) -> ( z e. ( U_ i e. I ( { i } X. J ) " { x } ) <-> x U_ i e. I ( { i } X. J ) z ) )
80 7 79 ax-mp 
 |-  ( z e. ( U_ i e. I ( { i } X. J ) " { x } ) <-> x U_ i e. I ( { i } X. J ) z )
81 df-br 
 |-  ( x U_ i e. I ( { i } X. J ) z <-> <. x , z >. e. U_ i e. I ( { i } X. J ) )
82 eliunxp 
 |-  ( <. x , z >. e. U_ i e. I ( { i } X. J ) <-> E. i E. j ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) )
83 80 81 82 3bitri 
 |-  ( z e. ( U_ i e. I ( { i } X. J ) " { x } ) <-> E. i E. j ( <. x , z >. = <. i , j >. /\ ( i e. I /\ j e. J ) ) )
84 78 83 bitr4di 
 |-  ( ( ph /\ x e. I ) -> ( z e. [_ x / i ]_ J <-> z e. ( U_ i e. I ( { i } X. J ) " { x } ) ) )
85 84 eqrdv 
 |-  ( ( ph /\ x e. I ) -> [_ x / i ]_ J = ( U_ i e. I ( { i } X. J ) " { x } ) )
86 85 mpteq1d 
 |-  ( ( ph /\ x e. I ) -> ( y e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) y ) ) = ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) )
87 51 86 syl5eq 
 |-  ( ( ph /\ x e. I ) -> ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) = ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) )
88 44 87 breqtrd 
 |-  ( ( ph /\ x e. I ) -> G dom DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) )
89 27 oveq2d 
 |-  ( ( ph /\ i e. I ) -> ( G DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) ) = ( G DProd ( j e. J |-> S ) ) )
90 89 mpteq2dva 
 |-  ( ph -> ( i e. I |-> ( G DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) ) ) = ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) )
91 3 90 breqtrrd 
 |-  ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) ) ) )
92 nfcv 
 |-  F/_ x ( G DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) )
93 nfcv 
 |-  F/_ i DProd
94 30 93 37 nfov 
 |-  F/_ i ( G DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) )
95 41 oveq2d 
 |-  ( i = x -> ( G DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) ) = ( G DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) ) )
96 92 94 95 cbvmpt 
 |-  ( i e. I |-> ( G DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) ) ) = ( x e. I |-> ( G DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) ) )
97 87 oveq2d 
 |-  ( ( ph /\ x e. I ) -> ( G DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) ) = ( G DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) ) )
98 97 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( G DProd ( j e. [_ x / i ]_ J |-> ( x ( i e. I , j e. J |-> S ) j ) ) ) ) = ( x e. I |-> ( G DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) ) ) )
99 96 98 syl5eq 
 |-  ( ph -> ( i e. I |-> ( G DProd ( j e. J |-> ( i ( i e. I , j e. J |-> S ) j ) ) ) ) = ( x e. I |-> ( G DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) ) ) )
100 91 99 breqtrd 
 |-  ( ph -> G dom DProd ( x e. I |-> ( G DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) ) ) )
101 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
102 8 12 21 88 100 101 dprd2da 
 |-  ( ph -> G dom DProd ( i e. I , j e. J |-> S ) )
103 8 12 21 88 100 101 dprd2db 
 |-  ( ph -> ( G DProd ( i e. I , j e. J |-> S ) ) = ( G DProd ( x e. I |-> ( G DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) ) ) ) )
104 99 90 eqtr3d 
 |-  ( ph -> ( x e. I |-> ( G DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) ) ) = ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) )
105 104 oveq2d 
 |-  ( ph -> ( G DProd ( x e. I |-> ( G DProd ( y e. ( U_ i e. I ( { i } X. J ) " { x } ) |-> ( x ( i e. I , j e. J |-> S ) y ) ) ) ) ) = ( G DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) ) )
106 103 105 eqtrd 
 |-  ( ph -> ( G DProd ( i e. I , j e. J |-> S ) ) = ( G DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) ) )
107 102 106 jca 
 |-  ( ph -> ( G dom DProd ( i e. I , j e. J |-> S ) /\ ( G DProd ( i e. I , j e. J |-> S ) ) = ( G DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) ) ) )