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 ffvelrnd
 |-  ( ( 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 ffvelrnd
 |-  ( ( 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 syl5eq
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 syl5eq
 |-  ( 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 ) ) )