Metamath Proof Explorer

Theorem symgcntz

Description: All elements of a (finite) set of permutations commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Hypotheses symgcntz.s 
|- S = ( SymGrp ` D )
symgcntz.b 
|- B = ( Base ` S )
symgcntz.z 
|- Z = ( Cntz ` S )
symgcntz.a 
|- ( ph -> A C_ B )
symgcntz.1 
|- ( ph -> Disj_ x e. A dom ( x \ _I ) )
Assertion symgcntz 
|- ( ph -> A C_ ( Z ` A ) )

Proof

Step Hyp Ref Expression
1 symgcntz.s 
 |-  S = ( SymGrp ` D )
2 symgcntz.b 
 |-  B = ( Base ` S )
3 symgcntz.z 
 |-  Z = ( Cntz ` S )
4 symgcntz.a 
 |-  ( ph -> A C_ B )
5 symgcntz.1 
 |-  ( ph -> Disj_ x e. A dom ( x \ _I ) )
6 simpr 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c = d ) -> c = d )
7 6 oveq1d 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c = d ) -> ( c ( +g ` S ) d ) = ( d ( +g ` S ) d ) )
8 6 oveq2d 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c = d ) -> ( d ( +g ` S ) c ) = ( d ( +g ` S ) d ) )
9 7 8 eqtr4d 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c = d ) -> ( c ( +g ` S ) d ) = ( d ( +g ` S ) c ) )
10 4 ad2antrr 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> A C_ B )
11 simplrl 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> c e. A )
12 10 11 sseldd 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> c e. B )
13 simplrr 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> d e. A )
14 10 13 sseldd 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> d e. B )
15 5 ad2antrr 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> Disj_ x e. A dom ( x \ _I ) )
16 simpr 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> c =/= d )
17 difeq1 
 |-  ( x = c -> ( x \ _I ) = ( c \ _I ) )
18 17 dmeqd 
 |-  ( x = c -> dom ( x \ _I ) = dom ( c \ _I ) )
19 difeq1 
 |-  ( x = d -> ( x \ _I ) = ( d \ _I ) )
20 19 dmeqd 
 |-  ( x = d -> dom ( x \ _I ) = dom ( d \ _I ) )
21 18 20 disji2 
 |-  ( ( Disj_ x e. A dom ( x \ _I ) /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( dom ( c \ _I ) i^i dom ( d \ _I ) ) = (/) )
22 15 11 13 16 21 syl121anc 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> ( dom ( c \ _I ) i^i dom ( d \ _I ) ) = (/) )
23 1 2 12 14 22 symgcom2 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> ( c o. d ) = ( d o. c ) )
24 eqid 
 |-  ( +g ` S ) = ( +g ` S )
25 1 2 24 symgov 
 |-  ( ( c e. B /\ d e. B ) -> ( c ( +g ` S ) d ) = ( c o. d ) )
26 12 14 25 syl2anc 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> ( c ( +g ` S ) d ) = ( c o. d ) )
27 1 2 24 symgov 
 |-  ( ( d e. B /\ c e. B ) -> ( d ( +g ` S ) c ) = ( d o. c ) )
28 14 12 27 syl2anc 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> ( d ( +g ` S ) c ) = ( d o. c ) )
29 23 26 28 3eqtr4d 
 |-  ( ( ( ph /\ ( c e. A /\ d e. A ) ) /\ c =/= d ) -> ( c ( +g ` S ) d ) = ( d ( +g ` S ) c ) )
30 9 29 pm2.61dane 
 |-  ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( c ( +g ` S ) d ) = ( d ( +g ` S ) c ) )
31 30 ralrimivva 
 |-  ( ph -> A. c e. A A. d e. A ( c ( +g ` S ) d ) = ( d ( +g ` S ) c ) )
32 2 24 3 sscntz 
 |-  ( ( A C_ B /\ A C_ B ) -> ( A C_ ( Z ` A ) <-> A. c e. A A. d e. A ( c ( +g ` S ) d ) = ( d ( +g ` S ) c ) ) )
33 4 4 32 syl2anc 
 |-  ( ph -> ( A C_ ( Z ` A ) <-> A. c e. A A. d e. A ( c ( +g ` S ) d ) = ( d ( +g ` S ) c ) ) )
34 31 33 mpbird 
 |-  ( ph -> A C_ ( Z ` A ) )