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 ) ) )