Metamath Proof Explorer


Theorem nmzbi

Description: Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypothesis elnmz.1 𝑁 = { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
Assertion nmzbi ( ( 𝐴𝑁𝐵𝑋 ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 𝑁 = { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
2 1 elnmz ( 𝐴𝑁 ↔ ( 𝐴𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ) )
3 2 simprbi ( 𝐴𝑁 → ∀ 𝑧𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) )
4 oveq2 ( 𝑧 = 𝐵 → ( 𝐴 + 𝑧 ) = ( 𝐴 + 𝐵 ) )
5 4 eleq1d ( 𝑧 = 𝐵 → ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝐴 + 𝐵 ) ∈ 𝑆 ) )
6 oveq1 ( 𝑧 = 𝐵 → ( 𝑧 + 𝐴 ) = ( 𝐵 + 𝐴 ) )
7 6 eleq1d ( 𝑧 = 𝐵 → ( ( 𝑧 + 𝐴 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) )
8 5 7 bibi12d ( 𝑧 = 𝐵 → ( ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ↔ ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) ) )
9 8 rspccva ( ( ∀ 𝑧𝑋 ( ( 𝐴 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝐴 ) ∈ 𝑆 ) ∧ 𝐵𝑋 ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) )
10 3 9 sylan ( ( 𝐴𝑁𝐵𝑋 ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) )