Metamath Proof Explorer

Theorem dprdss

Description: Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdss.1 
|- ( ph -> G dom DProd T )
dprdss.2 
|- ( ph -> dom T = I )
dprdss.3 
|- ( ph -> S : I --> ( SubGrp ` G ) )
dprdss.4 
|- ( ( ph /\ k e. I ) -> ( S ` k ) C_ ( T ` k ) )
Assertion dprdss 
|- ( ph -> ( G dom DProd S /\ ( G DProd S ) C_ ( G DProd T ) ) )

Proof

Step Hyp Ref Expression
1 dprdss.1 
 |-  ( ph -> G dom DProd T )
2 dprdss.2 
 |-  ( ph -> dom T = I )
3 dprdss.3 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
4 dprdss.4 
 |-  ( ( ph /\ k e. I ) -> ( S ` k ) C_ ( T ` k ) )
5 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
8 dprdgrp 
 |-  ( G dom DProd T -> G e. Grp )
9 1 8 syl 
 |-  ( ph -> G e. Grp )
10 1 2 dprddomcld 
 |-  ( ph -> I e. _V )
11 4 ralrimiva 
 |-  ( ph -> A. k e. I ( S ` k ) C_ ( T ` k ) )
12 fveq2 
 |-  ( k = x -> ( S ` k ) = ( S ` x ) )
13 fveq2 
 |-  ( k = x -> ( T ` k ) = ( T ` x ) )
14 12 13 sseq12d 
 |-  ( k = x -> ( ( S ` k ) C_ ( T ` k ) <-> ( S ` x ) C_ ( T ` x ) ) )
15 14 rspcv 
 |-  ( x e. I -> ( A. k e. I ( S ` k ) C_ ( T ` k ) -> ( S ` x ) C_ ( T ` x ) ) )
16 11 15 mpan9 
 |-  ( ( ph /\ x e. I ) -> ( S ` x ) C_ ( T ` x ) )
17 16 3ad2antr1 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( S ` x ) C_ ( T ` x ) )
18 1 adantr 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> G dom DProd T )
19 2 adantr 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> dom T = I )
20 simpr1 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> x e. I )
21 simpr2 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> y e. I )
22 simpr3 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> x =/= y )
23 18 19 20 21 22 5 dprdcntz 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( T ` x ) C_ ( ( Cntz ` G ) ` ( T ` y ) ) )
24 1 2 dprdf2 
 |-  ( ph -> T : I --> ( SubGrp ` G ) )
25 24 adantr 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> T : I --> ( SubGrp ` G ) )
26 25 21 ffvelrnd 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( T ` y ) e. ( SubGrp ` G ) )
27 eqid 
 |-  ( Base ` G ) = ( Base ` G )
28 27 subgss 
 |-  ( ( T ` y ) e. ( SubGrp ` G ) -> ( T ` y ) C_ ( Base ` G ) )
29 26 28 syl 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( T ` y ) C_ ( Base ` G ) )
30 fveq2 
 |-  ( k = y -> ( S ` k ) = ( S ` y ) )
31 fveq2 
 |-  ( k = y -> ( T ` k ) = ( T ` y ) )
32 30 31 sseq12d 
 |-  ( k = y -> ( ( S ` k ) C_ ( T ` k ) <-> ( S ` y ) C_ ( T ` y ) ) )
33 11 adantr 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> A. k e. I ( S ` k ) C_ ( T ` k ) )
34 32 33 21 rspcdva 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( S ` y ) C_ ( T ` y ) )
35 27 5 cntz2ss 
 |-  ( ( ( T ` y ) C_ ( Base ` G ) /\ ( S ` y ) C_ ( T ` y ) ) -> ( ( Cntz ` G ) ` ( T ` y ) ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
36 29 34 35 syl2anc 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( ( Cntz ` G ) ` ( T ` y ) ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
37 23 36 sstrd 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( T ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
38 17 37 sstrd 
 |-  ( ( ph /\ ( x e. I /\ y e. I /\ x =/= y ) ) -> ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
39 9 adantr 
 |-  ( ( ph /\ x e. I ) -> G e. Grp )
40 27 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
41 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
42 39 40 41 3syl 
 |-  ( ( ph /\ x e. I ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
43 difss 
 |-  ( I \ { x } ) C_ I
44 11 adantr 
 |-  ( ( ph /\ x e. I ) -> A. k e. I ( S ` k ) C_ ( T ` k ) )
45 ssralv 
 |-  ( ( I \ { x } ) C_ I -> ( A. k e. I ( S ` k ) C_ ( T ` k ) -> A. k e. ( I \ { x } ) ( S ` k ) C_ ( T ` k ) ) )
46 43 44 45 mpsyl 
 |-  ( ( ph /\ x e. I ) -> A. k e. ( I \ { x } ) ( S ` k ) C_ ( T ` k ) )
47 ss2iun 
 |-  ( A. k e. ( I \ { x } ) ( S ` k ) C_ ( T ` k ) -> U_ k e. ( I \ { x } ) ( S ` k ) C_ U_ k e. ( I \ { x } ) ( T ` k ) )
48 46 47 syl 
 |-  ( ( ph /\ x e. I ) -> U_ k e. ( I \ { x } ) ( S ` k ) C_ U_ k e. ( I \ { x } ) ( T ` k ) )
49 3 adantr 
 |-  ( ( ph /\ x e. I ) -> S : I --> ( SubGrp ` G ) )
50 ffun 
 |-  ( S : I --> ( SubGrp ` G ) -> Fun S )
51 funiunfv 
 |-  ( Fun S -> U_ k e. ( I \ { x } ) ( S ` k ) = U. ( S " ( I \ { x } ) ) )
52 49 50 51 3syl 
 |-  ( ( ph /\ x e. I ) -> U_ k e. ( I \ { x } ) ( S ` k ) = U. ( S " ( I \ { x } ) ) )
53 24 adantr 
 |-  ( ( ph /\ x e. I ) -> T : I --> ( SubGrp ` G ) )
54 ffun 
 |-  ( T : I --> ( SubGrp ` G ) -> Fun T )
55 funiunfv 
 |-  ( Fun T -> U_ k e. ( I \ { x } ) ( T ` k ) = U. ( T " ( I \ { x } ) ) )
56 53 54 55 3syl 
 |-  ( ( ph /\ x e. I ) -> U_ k e. ( I \ { x } ) ( T ` k ) = U. ( T " ( I \ { x } ) ) )
57 48 52 56 3sstr3d 
 |-  ( ( ph /\ x e. I ) -> U. ( S " ( I \ { x } ) ) C_ U. ( T " ( I \ { x } ) ) )
58 imassrn 
 |-  ( T " ( I \ { x } ) ) C_ ran T
59 53 frnd 
 |-  ( ( ph /\ x e. I ) -> ran T C_ ( SubGrp ` G ) )
60 mresspw 
 |-  ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
61 42 60 syl 
 |-  ( ( ph /\ x e. I ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
62 59 61 sstrd 
 |-  ( ( ph /\ x e. I ) -> ran T C_ ~P ( Base ` G ) )
63 58 62 sstrid 
 |-  ( ( ph /\ x e. I ) -> ( T " ( I \ { x } ) ) C_ ~P ( Base ` G ) )
64 sspwuni 
 |-  ( ( T " ( I \ { x } ) ) C_ ~P ( Base ` G ) <-> U. ( T " ( I \ { x } ) ) C_ ( Base ` G ) )
65 63 64 sylib 
 |-  ( ( ph /\ x e. I ) -> U. ( T " ( I \ { x } ) ) C_ ( Base ` G ) )
66 42 7 57 65 mrcssd 
 |-  ( ( ph /\ x e. I ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( T " ( I \ { x } ) ) ) )
67 ss2in 
 |-  ( ( ( S ` x ) C_ ( T ` x ) /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( T " ( I \ { x } ) ) ) ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ ( ( T ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( T " ( I \ { x } ) ) ) ) )
68 16 66 67 syl2anc 
 |-  ( ( ph /\ x e. I ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ ( ( T ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( T " ( I \ { x } ) ) ) ) )
69 1 adantr 
 |-  ( ( ph /\ x e. I ) -> G dom DProd T )
70 2 adantr 
 |-  ( ( ph /\ x e. I ) -> dom T = I )
71 simpr 
 |-  ( ( ph /\ x e. I ) -> x e. I )
72 69 70 71 6 7 dprddisj 
 |-  ( ( ph /\ x e. I ) -> ( ( T ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( T " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } )
73 68 72 sseqtrd 
 |-  ( ( ph /\ x e. I ) -> ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
74 5 6 7 9 10 3 38 73 dmdprdd 
 |-  ( ph -> G dom DProd S )
75 1 a1d 
 |-  ( ph -> ( G dom DProd S -> G dom DProd T ) )
76 ss2ixp 
 |-  ( A. k e. I ( S ` k ) C_ ( T ` k ) -> X_ k e. I ( S ` k ) C_ X_ k e. I ( T ` k ) )
77 11 76 syl 
 |-  ( ph -> X_ k e. I ( S ` k ) C_ X_ k e. I ( T ` k ) )
78 rabss2 
 |-  ( X_ k e. I ( S ` k ) C_ X_ k e. I ( T ` k ) -> { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } C_ { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } )
79 ssrexv 
 |-  ( { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } C_ { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } -> ( E. f e. { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) -> E. f e. { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) )
80 77 78 79 3syl 
 |-  ( ph -> ( E. f e. { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) -> E. f e. { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) )
81 75 80 anim12d 
 |-  ( ph -> ( ( G dom DProd S /\ E. f e. { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) -> ( G dom DProd T /\ E. f e. { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) ) )
82 fdm 
 |-  ( S : I --> ( SubGrp ` G ) -> dom S = I )
83 eqid 
 |-  { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } = { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) }
84 6 83 eldprd 
 |-  ( dom S = I -> ( a e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) ) )
85 3 82 84 3syl 
 |-  ( ph -> ( a e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. { h e. X_ k e. I ( S ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) ) )
86 eqid 
 |-  { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } = { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) }
87 6 86 eldprd 
 |-  ( dom T = I -> ( a e. ( G DProd T ) <-> ( G dom DProd T /\ E. f e. { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) ) )
88 2 87 syl 
 |-  ( ph -> ( a e. ( G DProd T ) <-> ( G dom DProd T /\ E. f e. { h e. X_ k e. I ( T ` k ) | h finSupp ( 0g ` G ) } a = ( G gsum f ) ) ) )
89 81 85 88 3imtr4d 
 |-  ( ph -> ( a e. ( G DProd S ) -> a e. ( G DProd T ) ) )
90 89 ssrdv 
 |-  ( ph -> ( G DProd S ) C_ ( G DProd T ) )
91 74 90 jca 
 |-  ( ph -> ( G dom DProd S /\ ( G DProd S ) C_ ( G DProd T ) ) )