Metamath Proof Explorer

Theorem dpjcntz

Description: The two subgroups that appear in dpjval commute. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 
|- ( ph -> G dom DProd S )
dpjfval.2 
|- ( ph -> dom S = I )
dpjlem.3 
|- ( ph -> X e. I )
dpjcntz.z 
|- Z = ( Cntz ` G )
Assertion dpjcntz 
|- ( ph -> ( S ` X ) C_ ( Z ` ( G DProd ( S |` ( I \ { X } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 
 |-  ( ph -> G dom DProd S )
2 dpjfval.2 
 |-  ( ph -> dom S = I )
3 dpjlem.3 
 |-  ( ph -> X e. I )
4 dpjcntz.z 
 |-  Z = ( Cntz ` G )
5 1 2 3 dpjlem 
 |-  ( ph -> ( G DProd ( S |` { X } ) ) = ( S ` X ) )
6 1 2 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
7 disjdif 
 |-  ( { X } i^i ( I \ { X } ) ) = (/)
8 7 a1i 
 |-  ( ph -> ( { X } i^i ( I \ { X } ) ) = (/) )
9 undif2 
 |-  ( { X } u. ( I \ { X } ) ) = ( { X } u. I )
10 3 snssd 
 |-  ( ph -> { X } C_ I )
11 ssequn1 
 |-  ( { X } C_ I <-> ( { X } u. I ) = I )
12 10 11 sylib 
 |-  ( ph -> ( { X } u. I ) = I )
13 9 12 eqtr2id 
 |-  ( ph -> I = ( { X } u. ( I \ { X } ) ) )
14 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
15 6 8 13 4 14 dmdprdsplit 
 |-  ( ph -> ( G dom DProd S <-> ( ( G dom DProd ( S |` { X } ) /\ G dom DProd ( S |` ( I \ { X } ) ) ) /\ ( G DProd ( S |` { X } ) ) C_ ( Z ` ( G DProd ( S |` ( I \ { X } ) ) ) ) /\ ( ( G DProd ( S |` { X } ) ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { ( 0g ` G ) } ) ) )
16 1 15 mpbid 
 |-  ( ph -> ( ( G dom DProd ( S |` { X } ) /\ G dom DProd ( S |` ( I \ { X } ) ) ) /\ ( G DProd ( S |` { X } ) ) C_ ( Z ` ( G DProd ( S |` ( I \ { X } ) ) ) ) /\ ( ( G DProd ( S |` { X } ) ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { ( 0g ` G ) } ) )
17 16 simp2d 
 |-  ( ph -> ( G DProd ( S |` { X } ) ) C_ ( Z ` ( G DProd ( S |` ( I \ { X } ) ) ) ) )
18 5 17 eqsstrrd 
 |-  ( ph -> ( S ` X ) C_ ( Z ` ( G DProd ( S |` ( I \ { X } ) ) ) ) )