Metamath Proof Explorer

Theorem rngrz

Description: The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009) Generalization of ringrz . (Revised by AV, 16-Feb-2025)

Ref Expression
Hypotheses rngcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rngcl.t ⊢ · = ( .r ‘ 𝑅 )
rnglz.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion rngrz ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 rngcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rngcl.t ⊢ · = ( .r ‘ 𝑅 )
3 rnglz.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
5 1 3 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
6 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
7 1 6 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ 0 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
8 4 5 7 syl2anc2 ⊢ ( 𝑅 ∈ Rng → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
9 8 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
10 9 oveq2d ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · ( 0 ( +g ‘ 𝑅 ) 0 ) ) = ( 𝑋 · 0 ) )
11 simpr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 1 3 rng0cl ⊢ ( 𝑅 ∈ Rng → 0 ∈ 𝐵 )
13 12 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
14 11 13 13 3jca ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) )
15 1 6 2 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ) → ( 𝑋 · ( 0 ( +g ‘ 𝑅 ) 0 ) ) = ( ( 𝑋 · 0 ) ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) )
16 14 15 syldan ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · ( 0 ( +g ‘ 𝑅 ) 0 ) ) = ( ( 𝑋 · 0 ) ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) )
17 4 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Grp )
18 1 2 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 · 0 ) ∈ 𝐵 )
19 13 18 mpd3an3 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) ∈ 𝐵 )
20 1 6 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 · 0 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) = ( 𝑋 · 0 ) )
21 20 eqcomd ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 · 0 ) ∈ 𝐵 ) → ( 𝑋 · 0 ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) )
22 17 19 21 syl2anc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) )
23 10 16 22 3eqtr3d ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 · 0 ) ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) )
24 1 6 grprcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑋 · 0 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ( 𝑋 · 0 ) ∈ 𝐵 ) ) → ( ( ( 𝑋 · 0 ) ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) ↔ ( 𝑋 · 0 ) = 0 ) )
25 17 19 13 19 24 syl13anc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑋 · 0 ) ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 · 0 ) ) ↔ ( 𝑋 · 0 ) = 0 ) )
26 23 25 mpbid ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )