Metamath Proof Explorer

Theorem dprdcntz

Description: The function S is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdcntz.1 
|- ( ph -> G dom DProd S )
dprdcntz.2 
|- ( ph -> dom S = I )
dprdcntz.3 
|- ( ph -> X e. I )
dprdcntz.4 
|- ( ph -> Y e. I )
dprdcntz.5 
|- ( ph -> X =/= Y )
dprdcntz.z 
|- Z = ( Cntz ` G )
Assertion dprdcntz 
|- ( ph -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) )

Proof

Step Hyp Ref Expression
1 dprdcntz.1 
 |-  ( ph -> G dom DProd S )
2 dprdcntz.2 
 |-  ( ph -> dom S = I )
3 dprdcntz.3 
 |-  ( ph -> X e. I )
4 dprdcntz.4 
 |-  ( ph -> Y e. I )
5 dprdcntz.5 
 |-  ( ph -> X =/= Y )
6 dprdcntz.z 
 |-  Z = ( Cntz ` G )
7 2fveq3 
 |-  ( y = Y -> ( Z ` ( S ` y ) ) = ( Z ` ( S ` Y ) ) )
8 7 sseq2d 
 |-  ( y = Y -> ( ( S ` X ) C_ ( Z ` ( S ` y ) ) <-> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) )
9 sneq 
 |-  ( x = X -> { x } = { X } )
10 9 difeq2d 
 |-  ( x = X -> ( I \ { x } ) = ( I \ { X } ) )
11 fveq2 
 |-  ( x = X -> ( S ` x ) = ( S ` X ) )
12 11 sseq1d 
 |-  ( x = X -> ( ( S ` x ) C_ ( Z ` ( S ` y ) ) <-> ( S ` X ) C_ ( Z ` ( S ` y ) ) ) )
13 10 12 raleqbidv 
 |-  ( x = X -> ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) <-> A. y e. ( I \ { X } ) ( S ` X ) C_ ( Z ` ( S ` y ) ) ) )
14 1 2 dprddomcld 
 |-  ( ph -> I e. _V )
15 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
16 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
17 6 15 16 dmdprd 
 |-  ( ( I e. _V /\ dom S = I ) -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
18 14 2 17 syl2anc 
 |-  ( ph -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) ) )
19 1 18 mpbid 
 |-  ( ph -> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) ) )
20 19 simp3d 
 |-  ( ph -> A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) )
21 simpl 
 |-  ( ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) -> A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) )
22 21 ralimi 
 |-  ( A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { x } ) ) ) ) = { ( 0g ` G ) } ) -> A. x e. I A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) )
23 20 22 syl 
 |-  ( ph -> A. x e. I A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) )
24 13 23 3 rspcdva 
 |-  ( ph -> A. y e. ( I \ { X } ) ( S ` X ) C_ ( Z ` ( S ` y ) ) )
25 5 necomd 
 |-  ( ph -> Y =/= X )
26 eldifsn 
 |-  ( Y e. ( I \ { X } ) <-> ( Y e. I /\ Y =/= X ) )
27 4 25 26 sylanbrc 
 |-  ( ph -> Y e. ( I \ { X } ) )
28 8 24 27 rspcdva 
 |-  ( ph -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) )