Metamath Proof Explorer

Theorem submcmn2

Description: A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses subgabl.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
submcmn2.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion submcmn2 ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐻 ∈ CMnd ↔ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 subgabl.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
2 submcmn2.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
3 1 submbas ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 1 4 ressplusg ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
6 5 oveqd ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
7 5 oveqd ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) )
8 6 7 eqeq12d ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
9 3 8 raleqbidv ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
10 3 9 raleqbidv ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 11 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 11 4 2 sscntz ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
14 12 12 13 syl2anc ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
15 1 submmnd ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐻 ∈ Mnd )
16 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
17 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
18 16 17 iscmn ⊢ ( 𝐻 ∈ CMnd ↔ ( 𝐻 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
19 18 baib ⊢ ( 𝐻 ∈ Mnd → ( 𝐻 ∈ CMnd ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
20 15 19 syl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐻 ∈ CMnd ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑥 ) ) )
21 10 14 20 3bitr4rd ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐻 ∈ CMnd ↔ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) )