Metamath Proof Explorer

Theorem rnglz

Description: The zero of a nonunital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 rngcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rngcl.t ⊢ · = ( .r ‘ 𝑅 )
3 rnglz.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
5 ablgrp ⊢ ( 𝑅 ∈ Abel → 𝑅 ∈ Grp )
6 4 5 syl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
7 1 3 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
8 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9 1 8 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ 0 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
10 6 7 9 syl2anc2 ⊢ ( 𝑅 ∈ Rng → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
11 10 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
12 11 oveq1d ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( 0 · 𝑋 ) )
13 simpl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Rng )
14 6 7 syl ⊢ ( 𝑅 ∈ Rng → 0 ∈ 𝐵 )
15 14 14 jca ⊢ ( 𝑅 ∈ Rng → ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) )
16 15 anim1i ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) )
17 df-3an ⊢ ( ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ↔ ( ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) )
18 16 17 sylibr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
19 1 8 2 rngdir ⊢ ( ( 𝑅 ∈ Rng ∧ ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) )
20 13 18 19 syl2anc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) )
21 6 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Grp )
22 14 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
23 simpr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
24 1 2 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) ∈ 𝐵 )
25 13 22 23 24 syl3anc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) ∈ 𝐵 )
26 1 8 3 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) → ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) = ( 0 · 𝑋 ) )
27 26 eqcomd ⊢ ( ( 𝑅 ∈ Grp ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
28 21 25 27 syl2anc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
29 12 20 28 3eqtr3d ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
30 1 8 grplcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 0 · 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) ) → ( ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) ↔ ( 0 · 𝑋 ) = 0 ) )
31 21 25 22 25 30 syl13anc ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) ↔ ( 0 · 𝑋 ) = 0 ) )
32 29 31 mpbid ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = 0 )