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