Metamath Proof Explorer


Theorem rngrz

Description: The zero of a non-unital ring is a right-absorbing element. (Contributed by AV, 16-Feb-2025)

Ref Expression
Hypotheses rngcl.b B = Base R
rngcl.t · ˙ = R
rnglz.z 0 ˙ = 0 R
Assertion rngrz R Rng X B X · ˙ 0 ˙ = 0 ˙

Proof

Step Hyp Ref Expression
1 rngcl.b B = Base R
2 rngcl.t · ˙ = R
3 rnglz.z 0 ˙ = 0 R
4 rnggrp R Rng R Grp
5 1 3 grpidcl R Grp 0 ˙ B
6 eqid + R = + R
7 1 6 3 grplid R Grp 0 ˙ B 0 ˙ + R 0 ˙ = 0 ˙
8 4 5 7 syl2anc2 R Rng 0 ˙ + R 0 ˙ = 0 ˙
9 8 adantr R Rng X B 0 ˙ + R 0 ˙ = 0 ˙
10 9 oveq2d R Rng X B X · ˙ 0 ˙ + R 0 ˙ = X · ˙ 0 ˙
11 simpr R Rng X B X B
12 1 3 rng0cl R Rng 0 ˙ B
13 12 adantr R Rng X B 0 ˙ B
14 11 13 13 3jca R Rng X B X B 0 ˙ B 0 ˙ B
15 1 6 2 rngdi R Rng X B 0 ˙ B 0 ˙ B X · ˙ 0 ˙ + R 0 ˙ = X · ˙ 0 ˙ + R X · ˙ 0 ˙
16 14 15 syldan R Rng X B X · ˙ 0 ˙ + R 0 ˙ = X · ˙ 0 ˙ + R X · ˙ 0 ˙
17 4 adantr R Rng X B R Grp
18 1 2 rngcl R Rng X B 0 ˙ B X · ˙ 0 ˙ B
19 13 18 mpd3an3 R Rng X B X · ˙ 0 ˙ B
20 1 6 3 grplid R Grp X · ˙ 0 ˙ B 0 ˙ + R X · ˙ 0 ˙ = X · ˙ 0 ˙
21 20 eqcomd R Grp X · ˙ 0 ˙ B X · ˙ 0 ˙ = 0 ˙ + R X · ˙ 0 ˙
22 17 19 21 syl2anc R Rng X B X · ˙ 0 ˙ = 0 ˙ + R X · ˙ 0 ˙
23 10 16 22 3eqtr3d R Rng X B X · ˙ 0 ˙ + R X · ˙ 0 ˙ = 0 ˙ + R X · ˙ 0 ˙
24 1 6 grprcan R Grp X · ˙ 0 ˙ B 0 ˙ B X · ˙ 0 ˙ B X · ˙ 0 ˙ + R X · ˙ 0 ˙ = 0 ˙ + R X · ˙ 0 ˙ X · ˙ 0 ˙ = 0 ˙
25 17 19 13 19 24 syl13anc R Rng X B X · ˙ 0 ˙ + R X · ˙ 0 ˙ = 0 ˙ + R X · ˙ 0 ˙ X · ˙ 0 ˙ = 0 ˙
26 23 25 mpbid R Rng X B X · ˙ 0 ˙ = 0 ˙