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

Metamath Proof Explorer

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