Theorem rrgeq0i

Description: Property of a left-regular element. (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	rrgeq0i	⊢ ( ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 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	1 2 3 4	isrrg	⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )
6	5	simprbi	⊢ ( 𝑋 ∈ 𝐸 → ∀ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) )
7		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
8	7	eqeq1d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 · 𝑦 ) = 0 ↔ ( 𝑋 · 𝑌 ) = 0 ) )
9		eqeq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 = 0 ↔ 𝑌 = 0 ) )
10	8 9	imbi12d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) ↔ ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) ) )
11	10	rspcv	⊢ ( 𝑌 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 0 → 𝑦 = 0 ) → ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) ) )
12	6 11	mpan9	⊢ ( ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) )