Metamath Proof Explorer


Theorem ringrz

Description: The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009)

Ref Expression
Hypotheses rngz.b B = Base R
rngz.t · ˙ = R
rngz.z 0 ˙ = 0 R
Assertion ringrz R Ring X B X · ˙ 0 ˙ = 0 ˙

Proof

Step Hyp Ref Expression
1 rngz.b B = Base R
2 rngz.t · ˙ = R
3 rngz.z 0 ˙ = 0 R
4 ringgrp R Ring 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 Ring 0 ˙ + R 0 ˙ = 0 ˙
9 8 adantr R Ring X B 0 ˙ + R 0 ˙ = 0 ˙
10 9 oveq2d R Ring X B X · ˙ 0 ˙ + R 0 ˙ = X · ˙ 0 ˙
11 simpr R Ring X B X B
12 4 5 syl R Ring 0 ˙ B
13 12 adantr R Ring X B 0 ˙ B
14 11 13 13 3jca R Ring X B X B 0 ˙ B 0 ˙ B
15 1 6 2 ringdi R Ring X B 0 ˙ B 0 ˙ B X · ˙ 0 ˙ + R 0 ˙ = X · ˙ 0 ˙ + R X · ˙ 0 ˙
16 14 15 syldan R Ring X B X · ˙ 0 ˙ + R 0 ˙ = X · ˙ 0 ˙ + R X · ˙ 0 ˙
17 4 adantr R Ring X B R Grp
18 1 2 ringcl R Ring X B 0 ˙ B X · ˙ 0 ˙ B
19 13 18 mpd3an3 R Ring 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 Ring X B X · ˙ 0 ˙ = 0 ˙ + R X · ˙ 0 ˙
23 10 16 22 3eqtr3d R Ring 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 Ring X B X · ˙ 0 ˙ + R X · ˙ 0 ˙ = 0 ˙ + R X · ˙ 0 ˙ X · ˙ 0 ˙ = 0 ˙
26 23 25 mpbid R Ring X B X · ˙ 0 ˙ = 0 ˙