Metamath Proof Explorer

Theorem dprdf1o

Description: Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdf1o.1 
|- ( ph -> G dom DProd S )
dprdf1o.2 
|- ( ph -> dom S = I )
dprdf1o.3 
|- ( ph -> F : J -1-1-onto-> I )
Assertion dprdf1o 
|- ( ph -> ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) = ( G DProd S ) ) )

Proof

Step Hyp Ref Expression
1 dprdf1o.1 
 |-  ( ph -> G dom DProd S )
2 dprdf1o.2 
 |-  ( ph -> dom S = I )
3 dprdf1o.3 
 |-  ( ph -> F : J -1-1-onto-> I )
4 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
5 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
6 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
7 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
8 1 7 syl 
 |-  ( ph -> G e. Grp )
9 f1of1 
 |-  ( F : J -1-1-onto-> I -> F : J -1-1-> I )
10 3 9 syl 
 |-  ( ph -> F : J -1-1-> I )
11 1 2 dprddomcld 
 |-  ( ph -> I e. _V )
12 f1dmex 
 |-  ( ( F : J -1-1-> I /\ I e. _V ) -> J e. _V )
13 10 11 12 syl2anc 
 |-  ( ph -> J e. _V )
14 1 2 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
15 f1of 
 |-  ( F : J -1-1-onto-> I -> F : J --> I )
16 3 15 syl 
 |-  ( ph -> F : J --> I )
17 fco 
 |-  ( ( S : I --> ( SubGrp ` G ) /\ F : J --> I ) -> ( S o. F ) : J --> ( SubGrp ` G ) )
18 14 16 17 syl2anc 
 |-  ( ph -> ( S o. F ) : J --> ( SubGrp ` G ) )
19 1 adantr 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> G dom DProd S )
20 2 adantr 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> dom S = I )
21 16 adantr 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> F : J --> I )
22 simpr1 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> x e. J )
23 21 22 ffvelcdmd 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( F ` x ) e. I )
24 simpr2 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> y e. J )
25 21 24 ffvelcdmd 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( F ` y ) e. I )
26 simpr3 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> x =/= y )
27 10 adantr 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> F : J -1-1-> I )
28 f1fveq 
 |-  ( ( F : J -1-1-> I /\ ( x e. J /\ y e. J ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
29 27 22 24 28 syl12anc 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
30 29 necon3bid 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( F ` x ) =/= ( F ` y ) <-> x =/= y ) )
31 26 30 mpbird 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( F ` x ) =/= ( F ` y ) )
32 19 20 23 25 31 4 dprdcntz 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( S ` ( F ` x ) ) C_ ( ( Cntz ` G ) ` ( S ` ( F ` y ) ) ) )
33 fvco3 
 |-  ( ( F : J --> I /\ x e. J ) -> ( ( S o. F ) ` x ) = ( S ` ( F ` x ) ) )
34 21 22 33 syl2anc 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( S o. F ) ` x ) = ( S ` ( F ` x ) ) )
35 fvco3 
 |-  ( ( F : J --> I /\ y e. J ) -> ( ( S o. F ) ` y ) = ( S ` ( F ` y ) ) )
36 21 24 35 syl2anc 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( S o. F ) ` y ) = ( S ` ( F ` y ) ) )
37 36 fveq2d 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( Cntz ` G ) ` ( ( S o. F ) ` y ) ) = ( ( Cntz ` G ) ` ( S ` ( F ` y ) ) ) )
38 32 34 37 3sstr4d 
 |-  ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( S o. F ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S o. F ) ` y ) ) )
39 16 33 sylan 
 |-  ( ( ph /\ x e. J ) -> ( ( S o. F ) ` x ) = ( S ` ( F ` x ) ) )
40 imaco 
 |-  ( ( S o. F ) " ( J \ { x } ) ) = ( S " ( F " ( J \ { x } ) ) )
41 3 adantr 
 |-  ( ( ph /\ x e. J ) -> F : J -1-1-onto-> I )
42 dff1o3 
 |-  ( F : J -1-1-onto-> I <-> ( F : J -onto-> I /\ Fun `' F ) )
43 42 simprbi 
 |-  ( F : J -1-1-onto-> I -> Fun `' F )
44 imadif 
 |-  ( Fun `' F -> ( F " ( J \ { x } ) ) = ( ( F " J ) \ ( F " { x } ) ) )
45 41 43 44 3syl 
 |-  ( ( ph /\ x e. J ) -> ( F " ( J \ { x } ) ) = ( ( F " J ) \ ( F " { x } ) ) )
46 f1ofo 
 |-  ( F : J -1-1-onto-> I -> F : J -onto-> I )
47 foima 
 |-  ( F : J -onto-> I -> ( F " J ) = I )
48 41 46 47 3syl 
 |-  ( ( ph /\ x e. J ) -> ( F " J ) = I )
49 f1ofn 
 |-  ( F : J -1-1-onto-> I -> F Fn J )
50 3 49 syl 
 |-  ( ph -> F Fn J )
51 fnsnfv 
 |-  ( ( F Fn J /\ x e. J ) -> { ( F ` x ) } = ( F " { x } ) )
52 50 51 sylan 
 |-  ( ( ph /\ x e. J ) -> { ( F ` x ) } = ( F " { x } ) )
53 52 eqcomd 
 |-  ( ( ph /\ x e. J ) -> ( F " { x } ) = { ( F ` x ) } )
54 48 53 difeq12d 
 |-  ( ( ph /\ x e. J ) -> ( ( F " J ) \ ( F " { x } ) ) = ( I \ { ( F ` x ) } ) )
55 45 54 eqtrd 
 |-  ( ( ph /\ x e. J ) -> ( F " ( J \ { x } ) ) = ( I \ { ( F ` x ) } ) )
56 55 imaeq2d 
 |-  ( ( ph /\ x e. J ) -> ( S " ( F " ( J \ { x } ) ) ) = ( S " ( I \ { ( F ` x ) } ) ) )
57 40 56 eqtrid 
 |-  ( ( ph /\ x e. J ) -> ( ( S o. F ) " ( J \ { x } ) ) = ( S " ( I \ { ( F ` x ) } ) ) )
58 57 unieqd 
 |-  ( ( ph /\ x e. J ) -> U. ( ( S o. F ) " ( J \ { x } ) ) = U. ( S " ( I \ { ( F ` x ) } ) ) )
59 58 fveq2d 
 |-  ( ( ph /\ x e. J ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { ( F ` x ) } ) ) ) )
60 39 59 ineq12d 
 |-  ( ( ph /\ x e. J ) -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) = ( ( S ` ( F ` x ) ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { ( F ` x ) } ) ) ) ) )
61 1 adantr 
 |-  ( ( ph /\ x e. J ) -> G dom DProd S )
62 2 adantr 
 |-  ( ( ph /\ x e. J ) -> dom S = I )
63 16 ffvelcdmda 
 |-  ( ( ph /\ x e. J ) -> ( F ` x ) e. I )
64 61 62 63 5 6 dprddisj 
 |-  ( ( ph /\ x e. J ) -> ( ( S ` ( F ` x ) ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { ( F ` x ) } ) ) ) ) = { ( 0g ` G ) } )
65 60 64 eqtrd 
 |-  ( ( ph /\ x e. J ) -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) = { ( 0g ` G ) } )
66 eqimss 
 |-  ( ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) = { ( 0g ` G ) } -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
67 65 66 syl 
 |-  ( ( ph /\ x e. J ) -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
68 4 5 6 8 13 18 38 67 dmdprdd 
 |-  ( ph -> G dom DProd ( S o. F ) )
69 rnco2 
 |-  ran ( S o. F ) = ( S " ran F )
70 forn 
 |-  ( F : J -onto-> I -> ran F = I )
71 3 46 70 3syl 
 |-  ( ph -> ran F = I )
72 71 imaeq2d 
 |-  ( ph -> ( S " ran F ) = ( S " I ) )
73 ffn 
 |-  ( S : I --> ( SubGrp ` G ) -> S Fn I )
74 fnima 
 |-  ( S Fn I -> ( S " I ) = ran S )
75 14 73 74 3syl 
 |-  ( ph -> ( S " I ) = ran S )
76 72 75 eqtrd 
 |-  ( ph -> ( S " ran F ) = ran S )
77 69 76 eqtrid 
 |-  ( ph -> ran ( S o. F ) = ran S )
78 77 unieqd 
 |-  ( ph -> U. ran ( S o. F ) = U. ran S )
79 78 fveq2d 
 |-  ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S o. F ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) )
80 6 dprdspan 
 |-  ( G dom DProd ( S o. F ) -> ( G DProd ( S o. F ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S o. F ) ) )
81 68 80 syl 
 |-  ( ph -> ( G DProd ( S o. F ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S o. F ) ) )
82 6 dprdspan 
 |-  ( G dom DProd S -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) )
83 1 82 syl 
 |-  ( ph -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) )
84 79 81 83 3eqtr4d 
 |-  ( ph -> ( G DProd ( S o. F ) ) = ( G DProd S ) )
85 68 84 jca 
 |-  ( ph -> ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) = ( G DProd S ) ) )