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	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	symgcntz.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	symgcntz.z	⊢ 𝑍 = ( Cntz ‘ 𝑆 )
	symgcntz.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	symgcntz.1	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 dom ( 𝑥 ∖ I ) )
Assertion	symgcntz	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑍 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		symgcntz.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		symgcntz.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		symgcntz.z	⊢ 𝑍 = ( Cntz ‘ 𝑆 )
4		symgcntz.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5		symgcntz.1	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 dom ( 𝑥 ∖ I ) )
6		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 = 𝑑 ) → 𝑐 = 𝑑 )
7	6	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 = 𝑑 ) → ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑑 ) )
8	6	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 = 𝑑 ) → ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑑 ) )
9	7 8	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 = 𝑑 ) → ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) )
10	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → 𝐴 ⊆ 𝐵 )
11		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → 𝑐 ∈ 𝐴 )
12	10 11	sseldd	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → 𝑐 ∈ 𝐵 )
13		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → 𝑑 ∈ 𝐴 )
14	10 13	sseldd	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → 𝑑 ∈ 𝐵 )
15	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → Disj 𝑥 ∈ 𝐴 dom ( 𝑥 ∖ I ) )
16		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → 𝑐 ≠ 𝑑 )
17		difeq1	⊢ ( 𝑥 = 𝑐 → ( 𝑥 ∖ I ) = ( 𝑐 ∖ I ) )
18	17	dmeqd	⊢ ( 𝑥 = 𝑐 → dom ( 𝑥 ∖ I ) = dom ( 𝑐 ∖ I ) )
19		difeq1	⊢ ( 𝑥 = 𝑑 → ( 𝑥 ∖ I ) = ( 𝑑 ∖ I ) )
20	19	dmeqd	⊢ ( 𝑥 = 𝑑 → dom ( 𝑥 ∖ I ) = dom ( 𝑑 ∖ I ) )
21	18 20	disji2	⊢ ( ( Disj 𝑥 ∈ 𝐴 dom ( 𝑥 ∖ I ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ 𝑐 ≠ 𝑑 ) → ( dom ( 𝑐 ∖ I ) ∩ dom ( 𝑑 ∖ I ) ) = ∅ )
22	15 11 13 16 21	syl121anc	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → ( dom ( 𝑐 ∖ I ) ∩ dom ( 𝑑 ∖ I ) ) = ∅ )
23	1 2 12 14 22	symgcom2	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → ( 𝑐 ∘ 𝑑 ) = ( 𝑑 ∘ 𝑐 ) )
24		eqid	⊢ ( +_g ‘ 𝑆 ) = ( +_g ‘ 𝑆 )
25	1 2 24	symgov	⊢ ( ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑐 ∘ 𝑑 ) )
26	12 14 25	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑐 ∘ 𝑑 ) )
27	1 2 24	symgov	⊢ ( ( 𝑑 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) = ( 𝑑 ∘ 𝑐 ) )
28	14 12 27	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) = ( 𝑑 ∘ 𝑐 ) )
29	23 26 28	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) ∧ 𝑐 ≠ 𝑑 ) → ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) )
30	9 29	pm2.61dane	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) )
31	30	ralrimivva	⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐴 ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) )
32	2 24 3	sscntz	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ⊆ ( 𝑍 ‘ 𝐴 ) ↔ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐴 ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) ) )
33	4 4 32	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊆ ( 𝑍 ‘ 𝐴 ) ↔ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐴 ( 𝑐 ( +_g ‘ 𝑆 ) 𝑑 ) = ( 𝑑 ( +_g ‘ 𝑆 ) 𝑐 ) ) )
34	31 33	mpbird	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑍 ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem symgcntz

Proof