Theorem cntz2ss

Description: Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	cntzrec.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzrec.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntz2ss	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		cntzrec.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzrec.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
4	3 2	cntzi	⊢ ( ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
5	4	ralrimiva	⊢ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
6		ssralv	⊢ ( 𝑇 ⊆ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) → ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) )
7	6	adantl	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) → ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) )
8	5 7	syl5	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) → ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) )
9	8	ralrimiv	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
10	1 2	cntzssv	⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵
11		sstr	⊢ ( ( 𝑇 ⊆ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → 𝑇 ⊆ 𝐵 )
12	11	ancoms	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝐵 )
13	1 3 2	sscntz	⊢ ( ( ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑇 ) ↔ ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) )
14	10 12 13	sylancr	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → ( ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑇 ) ↔ ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) )
15	9 14	mpbird	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑇 ) )