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 )