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

Metamath Proof Explorer

Theorem isrrg

Description: Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypotheses rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rrgval.t ⊢ · = ( .r ‘ 𝑅 )
rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion isrrg ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2 rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 rrgval.t ⊢ · = ( .r ‘ 𝑅 )
4 rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑦 ) )
6 5 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 · 𝑦 ) = 0 ↔ ( 𝑋 · 𝑦 ) = 0 ) )
7 6 imbi1d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) ↔ ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )
8 7 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )
9 1 2 3 4 rrgval ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) }
10 8 9 elrab2 ⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )