Metamath Proof Explorer

Theorem dprdres

Description: Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdres.1 
|- ( ph -> G dom DProd S )
dprdres.2 
|- ( ph -> dom S = I )
dprdres.3 
|- ( ph -> A C_ I )
Assertion dprdres 
|- ( ph -> ( G dom DProd ( S |` A ) /\ ( G DProd ( S |` A ) ) C_ ( G DProd S ) ) )

Proof

Step Hyp Ref Expression
1 dprdres.1 
 |-  ( ph -> G dom DProd S )
2 dprdres.2 
 |-  ( ph -> dom S = I )
3 dprdres.3 
 |-  ( ph -> A C_ I )
4 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
5 1 4 syl 
 |-  ( ph -> G e. Grp )
6 1 2 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
7 6 3 fssresd 
 |-  ( ph -> ( S |` A ) : A --> ( SubGrp ` G ) )
8 1 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> G dom DProd S )
9 2 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> dom S = I )
10 3 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> A C_ I )
11 simplr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> x e. A )
12 10 11 sseldd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> x e. I )
13 eldifi 
 |-  ( y e. ( A \ { x } ) -> y e. A )
14 13 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> y e. A )
15 10 14 sseldd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> y e. I )
16 eldifsni 
 |-  ( y e. ( A \ { x } ) -> y =/= x )
17 16 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> y =/= x )
18 17 necomd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> x =/= y )
19 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
20 8 9 12 15 18 19 dprdcntz 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
21 11 fvresd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( S |` A ) ` x ) = ( S ` x ) )
22 14 fvresd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( S |` A ) ` y ) = ( S ` y ) )
23 22 fveq2d 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) = ( ( Cntz ` G ) ` ( S ` y ) ) )
24 20 21 23 3sstr4d 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A \ { x } ) ) -> ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) )
25 24 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) )
26 fvres 
 |-  ( x e. A -> ( ( S |` A ) ` x ) = ( S ` x ) )
27 26 adantl 
 |-  ( ( ph /\ x e. A ) -> ( ( S |` A ) ` x ) = ( S ` x ) )
28 27 ineq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) )
29 eqid 
 |-  ( Base ` G ) = ( Base ` G )
30 29 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
31 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
32 5 30 31 3syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
33 32 adantr 
 |-  ( ( ph /\ x e. A ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
34 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
35 resss 
 |-  ( S |` A ) C_ S
36 imass1 
 |-  ( ( S |` A ) C_ S -> ( ( S |` A ) " ( A \ { x } ) ) C_ ( S " ( A \ { x } ) ) )
37 35 36 ax-mp 
 |-  ( ( S |` A ) " ( A \ { x } ) ) C_ ( S " ( A \ { x } ) )
38 3 adantr 
 |-  ( ( ph /\ x e. A ) -> A C_ I )
39 ssdif 
 |-  ( A C_ I -> ( A \ { x } ) C_ ( I \ { x } ) )
40 imass2 
 |-  ( ( A \ { x } ) C_ ( I \ { x } ) -> ( S " ( A \ { x } ) ) C_ ( S " ( I \ { x } ) ) )
41 38 39 40 3syl 
 |-  ( ( ph /\ x e. A ) -> ( S " ( A \ { x } ) ) C_ ( S " ( I \ { x } ) ) )
42 37 41 sstrid 
 |-  ( ( ph /\ x e. A ) -> ( ( S |` A ) " ( A \ { x } ) ) C_ ( S " ( I \ { x } ) ) )
43 42 unissd 
 |-  ( ( ph /\ x e. A ) -> U. ( ( S |` A ) " ( A \ { x } ) ) C_ U. ( S " ( I \ { x } ) ) )
44 imassrn 
 |-  ( S " ( I \ { x } ) ) C_ ran S
45 6 frnd 
 |-  ( ph -> ran S C_ ( SubGrp ` G ) )
46 29 subgss 
 |-  ( x e. ( SubGrp ` G ) -> x C_ ( Base ` G ) )
47 velpw 
 |-  ( x e. ~P ( Base ` G ) <-> x C_ ( Base ` G ) )
48 46 47 sylibr 
 |-  ( x e. ( SubGrp ` G ) -> x e. ~P ( Base ` G ) )
49 48 ssriv 
 |-  ( SubGrp ` G ) C_ ~P ( Base ` G )
50 45 49 sstrdi 
 |-  ( ph -> ran S C_ ~P ( Base ` G ) )
51 50 adantr 
 |-  ( ( ph /\ x e. A ) -> ran S C_ ~P ( Base ` G ) )
52 44 51 sstrid 
 |-  ( ( ph /\ x e. A ) -> ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) )
53 sspwuni 
 |-  ( ( S " ( I \ { x } ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) )
54 52 53 sylib 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( I \ { x } ) ) C_ ( Base ` G ) )
55 33 34 43 54 mrcssd 
 |-  ( ( ph /\ x e. A ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) )
56 sslin 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) C_ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) )
57 55 56 syl 
 |-  ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) C_ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) )
58 1 adantr 
 |-  ( ( ph /\ x e. A ) -> G dom DProd S )
59 2 adantr 
 |-  ( ( ph /\ x e. A ) -> dom S = I )
60 3 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. I )
61 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
62 58 59 60 61 34 dprddisj 
 |-  ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } )
63 57 62 sseqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
64 6 ffvelcdmda 
 |-  ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) )
65 60 64 syldan 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) e. ( SubGrp ` G ) )
66 61 subg0cl 
 |-  ( ( S ` x ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( S ` x ) )
67 65 66 syl 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( S ` x ) )
68 43 54 sstrd 
 |-  ( ( ph /\ x e. A ) -> U. ( ( S |` A ) " ( A \ { x } ) ) C_ ( Base ` G ) )
69 34 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( ( S |` A ) " ( A \ { x } ) ) C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) e. ( SubGrp ` G ) )
70 33 68 69 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) e. ( SubGrp ` G ) )
71 61 subg0cl 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) )
72 70 71 syl 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) )
73 67 72 elind 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) )
74 73 snssd 
 |-  ( ( ph /\ x e. A ) -> { ( 0g ` G ) } C_ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) )
75 63 74 eqssd 
 |-  ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } )
76 28 75 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } )
77 25 76 jca 
 |-  ( ( ph /\ x e. A ) -> ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) )
78 77 ralrimiva 
 |-  ( ph -> A. x e. A ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) )
79 1 2 dprddomcld 
 |-  ( ph -> I e. _V )
80 79 3 ssexd 
 |-  ( ph -> A e. _V )
81 7 fdmd 
 |-  ( ph -> dom ( S |` A ) = A )
82 19 61 34 dmdprd 
 |-  ( ( A e. _V /\ dom ( S |` A ) = A ) -> ( G dom DProd ( S |` A ) <-> ( G e. Grp /\ ( S |` A ) : A --> ( SubGrp ` G ) /\ A. x e. A ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
83 80 81 82 syl2anc 
 |-  ( ph -> ( G dom DProd ( S |` A ) <-> ( G e. Grp /\ ( S |` A ) : A --> ( SubGrp ` G ) /\ A. x e. A ( A. y e. ( A \ { x } ) ( ( S |` A ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S |` A ) ` y ) ) /\ ( ( ( S |` A ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S |` A ) " ( A \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
84 5 7 78 83 mpbir3and 
 |-  ( ph -> G dom DProd ( S |` A ) )
85 rnss 
 |-  ( ( S |` A ) C_ S -> ran ( S |` A ) C_ ran S )
86 uniss 
 |-  ( ran ( S |` A ) C_ ran S -> U. ran ( S |` A ) C_ U. ran S )
87 35 85 86 mp2b 
 |-  U. ran ( S |` A ) C_ U. ran S
88 87 a1i 
 |-  ( ph -> U. ran ( S |` A ) C_ U. ran S )
89 sspwuni 
 |-  ( ran S C_ ~P ( Base ` G ) <-> U. ran S C_ ( Base ` G ) )
90 50 89 sylib 
 |-  ( ph -> U. ran S C_ ( Base ` G ) )
91 32 34 88 90 mrcssd 
 |-  ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S |` A ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) )
92 34 dprdspan 
 |-  ( G dom DProd ( S |` A ) -> ( G DProd ( S |` A ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S |` A ) ) )
93 84 92 syl 
 |-  ( ph -> ( G DProd ( S |` A ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S |` A ) ) )
94 34 dprdspan 
 |-  ( G dom DProd S -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) )
95 1 94 syl 
 |-  ( ph -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) )
96 91 93 95 3sstr4d 
 |-  ( ph -> ( G DProd ( S |` A ) ) C_ ( G DProd S ) )
97 84 96 jca 
 |-  ( ph -> ( G dom DProd ( S |` A ) /\ ( G DProd ( S |` A ) ) C_ ( G DProd S ) ) )