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

Metamath Proof Explorer

Theorem cntzrec

Description: Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 cntzrec.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntzrec.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3 ralcom ⊢ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑇 ∀ 𝑥 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
4 eqcom ⊢ ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ↔ ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
5 4 2ralbii ⊢ ( ∀ 𝑦 ∈ 𝑇 ∀ 𝑥 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑇 ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
6 3 5 bitri ⊢ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑇 ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
7 6 a1i ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑇 ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) )
8 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
9 1 8 2 sscntz ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ) )
10 1 8 2 sscntz ⊢ ( ( 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑇 ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) )
11 10 ancoms ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑇 ⊆ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑇 ∀ 𝑥 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) )
12 7 9 11 3bitr4d ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ↔ 𝑇 ⊆ ( 𝑍 ‘ 𝑆 ) ) )