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