Theorem elnmz

Description: Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypothesis	elnmz.1	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
Assertion	elnmz	⊢ ( 𝐴 ∈ 𝑁 ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elnmz.1	⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
2		oveq2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑧 ) )
3	2	eleq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑥 + 𝑧 ) ∈ 𝑆 ) )
4		oveq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 + 𝑥 ) = ( 𝑧 + 𝑥 ) )
5	4	eleq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) )
6	3 5	bibi12d	⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ) )
7	6	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) )
8		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 + 𝑧 ) = ( 𝐴 + 𝑧 ) )
9	8	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝐴 + 𝑧 ) ∈ 𝑆 ) )
10		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑧 + 𝑥 ) = ( 𝑧 + 𝐴 ) )
11	10	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) )
12	9 11	bibi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )
13	12	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )
14	7 13	bitrid	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )
15	14 1	elrab2	⊢ ( 𝐴 ∈ 𝑁 ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )