Metamath Proof Explorer

Theorem dprdcntz2

Description: The function S is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dprdcntz2.1 
|- ( ph -> G dom DProd S )
dprdcntz2.2 
|- ( ph -> dom S = I )
dprdcntz2.c 
|- ( ph -> C C_ I )
dprdcntz2.d 
|- ( ph -> D C_ I )
dprdcntz2.i 
|- ( ph -> ( C i^i D ) = (/) )
dprdcntz2.z 
|- Z = ( Cntz ` G )
Assertion dprdcntz2 
|- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )

Proof

Step Hyp Ref Expression
1 dprdcntz2.1 
 |-  ( ph -> G dom DProd S )
2 dprdcntz2.2 
 |-  ( ph -> dom S = I )
3 dprdcntz2.c 
 |-  ( ph -> C C_ I )
4 dprdcntz2.d 
 |-  ( ph -> D C_ I )
5 dprdcntz2.i 
 |-  ( ph -> ( C i^i D ) = (/) )
6 dprdcntz2.z 
 |-  Z = ( Cntz ` G )
7 1 2 3 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` C ) /\ ( G DProd ( S |` C ) ) C_ ( G DProd S ) ) )
8 7 simpld 
 |-  ( ph -> G dom DProd ( S |` C ) )
9 dmres 
 |-  dom ( S |` C ) = ( C i^i dom S )
10 3 2 sseqtrrd 
 |-  ( ph -> C C_ dom S )
11 df-ss 
 |-  ( C C_ dom S <-> ( C i^i dom S ) = C )
12 10 11 sylib 
 |-  ( ph -> ( C i^i dom S ) = C )
13 9 12 syl5eq 
 |-  ( ph -> dom ( S |` C ) = C )
14 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
15 1 14 syl 
 |-  ( ph -> G e. Grp )
16 eqid 
 |-  ( Base ` G ) = ( Base ` G )
17 16 dprdssv 
 |-  ( G DProd ( S |` D ) ) C_ ( Base ` G )
18 16 6 cntzsubg 
 |-  ( ( G e. Grp /\ ( G DProd ( S |` D ) ) C_ ( Base ` G ) ) -> ( Z ` ( G DProd ( S |` D ) ) ) e. ( SubGrp ` G ) )
19 15 17 18 sylancl 
 |-  ( ph -> ( Z ` ( G DProd ( S |` D ) ) ) e. ( SubGrp ` G ) )
20 fvres 
 |-  ( x e. C -> ( ( S |` C ) ` x ) = ( S ` x ) )
21 20 adantl 
 |-  ( ( ph /\ x e. C ) -> ( ( S |` C ) ` x ) = ( S ` x ) )
22 1 2 4 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` D ) /\ ( G DProd ( S |` D ) ) C_ ( G DProd S ) ) )
23 22 simpld 
 |-  ( ph -> G dom DProd ( S |` D ) )
24 23 adantr 
 |-  ( ( ph /\ x e. C ) -> G dom DProd ( S |` D ) )
25 dprdsubg 
 |-  ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
26 24 25 syl 
 |-  ( ( ph /\ x e. C ) -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
27 3 sselda 
 |-  ( ( ph /\ x e. C ) -> x e. I )
28 1 2 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
29 28 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) )
30 27 29 syldan 
 |-  ( ( ph /\ x e. C ) -> ( S ` x ) e. ( SubGrp ` G ) )
31 dmres 
 |-  dom ( S |` D ) = ( D i^i dom S )
32 4 2 sseqtrrd 
 |-  ( ph -> D C_ dom S )
33 df-ss 
 |-  ( D C_ dom S <-> ( D i^i dom S ) = D )
34 32 33 sylib 
 |-  ( ph -> ( D i^i dom S ) = D )
35 31 34 syl5eq 
 |-  ( ph -> dom ( S |` D ) = D )
36 35 adantr 
 |-  ( ( ph /\ x e. C ) -> dom ( S |` D ) = D )
37 15 adantr 
 |-  ( ( ph /\ x e. C ) -> G e. Grp )
38 16 subgss 
 |-  ( ( S ` x ) e. ( SubGrp ` G ) -> ( S ` x ) C_ ( Base ` G ) )
39 30 38 syl 
 |-  ( ( ph /\ x e. C ) -> ( S ` x ) C_ ( Base ` G ) )
40 16 6 cntzsubg 
 |-  ( ( G e. Grp /\ ( S ` x ) C_ ( Base ` G ) ) -> ( Z ` ( S ` x ) ) e. ( SubGrp ` G ) )
41 37 39 40 syl2anc 
 |-  ( ( ph /\ x e. C ) -> ( Z ` ( S ` x ) ) e. ( SubGrp ` G ) )
42 fvres 
 |-  ( y e. D -> ( ( S |` D ) ` y ) = ( S ` y ) )
43 42 adantl 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( S |` D ) ` y ) = ( S ` y ) )
44 1 ad2antrr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> G dom DProd S )
45 2 ad2antrr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> dom S = I )
46 4 adantr 
 |-  ( ( ph /\ x e. C ) -> D C_ I )
47 46 sselda 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> y e. I )
48 27 adantr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> x e. I )
49 simpr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> y e. D )
50 noel 
 |-  -. x e. (/)
51 elin 
 |-  ( x e. ( C i^i D ) <-> ( x e. C /\ x e. D ) )
52 5 eleq2d 
 |-  ( ph -> ( x e. ( C i^i D ) <-> x e. (/) ) )
53 51 52 bitr3id 
 |-  ( ph -> ( ( x e. C /\ x e. D ) <-> x e. (/) ) )
54 50 53 mtbiri 
 |-  ( ph -> -. ( x e. C /\ x e. D ) )
55 imnan 
 |-  ( ( x e. C -> -. x e. D ) <-> -. ( x e. C /\ x e. D ) )
56 54 55 sylibr 
 |-  ( ph -> ( x e. C -> -. x e. D ) )
57 56 imp 
 |-  ( ( ph /\ x e. C ) -> -. x e. D )
58 57 adantr 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> -. x e. D )
59 nelne2 
 |-  ( ( y e. D /\ -. x e. D ) -> y =/= x )
60 49 58 59 syl2anc 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> y =/= x )
61 44 45 47 48 60 6 dprdcntz 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( S ` y ) C_ ( Z ` ( S ` x ) ) )
62 43 61 eqsstrd 
 |-  ( ( ( ph /\ x e. C ) /\ y e. D ) -> ( ( S |` D ) ` y ) C_ ( Z ` ( S ` x ) ) )
63 24 36 41 62 dprdlub 
 |-  ( ( ph /\ x e. C ) -> ( G DProd ( S |` D ) ) C_ ( Z ` ( S ` x ) ) )
64 6 26 30 63 cntzrecd 
 |-  ( ( ph /\ x e. C ) -> ( S ` x ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
65 21 64 eqsstrd 
 |-  ( ( ph /\ x e. C ) -> ( ( S |` C ) ` x ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
66 8 13 19 65 dprdlub 
 |-  ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )