This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑇 ) )