# Metamath Proof Explorer

## Theorem rngolz

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

Ref Expression
Hypotheses ringlz.1 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
ringlz.2 ${⊢}{X}=\mathrm{ran}{G}$
ringlz.3 ${⊢}{G}={1}^{st}\left({R}\right)$
ringlz.4 ${⊢}{H}={2}^{nd}\left({R}\right)$
Assertion rngolz ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {Z}{H}{A}={Z}$

### Proof

Step Hyp Ref Expression
1 ringlz.1 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
2 ringlz.2 ${⊢}{X}=\mathrm{ran}{G}$
3 ringlz.3 ${⊢}{G}={1}^{st}\left({R}\right)$
4 ringlz.4 ${⊢}{H}={2}^{nd}\left({R}\right)$
5 3 rngogrpo ${⊢}{R}\in \mathrm{RingOps}\to {G}\in \mathrm{GrpOp}$
6 2 1 grpoidcl ${⊢}{G}\in \mathrm{GrpOp}\to {Z}\in {X}$
7 2 1 grpolid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {Z}\in {X}\right)\to {Z}{G}{Z}={Z}$
8 5 6 7 syl2anc2 ${⊢}{R}\in \mathrm{RingOps}\to {Z}{G}{Z}={Z}$
9 8 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {Z}{G}{Z}={Z}$
10 9 oveq1d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({Z}{G}{Z}\right){H}{A}={Z}{H}{A}$
11 3 2 1 rngo0cl ${⊢}{R}\in \mathrm{RingOps}\to {Z}\in {X}$
12 11 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {Z}\in {X}$
13 simpr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {A}\in {X}$
14 12 12 13 3jca ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({Z}\in {X}\wedge {Z}\in {X}\wedge {A}\in {X}\right)$
15 3 4 2 rngodir ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({Z}\in {X}\wedge {Z}\in {X}\wedge {A}\in {X}\right)\right)\to \left({Z}{G}{Z}\right){H}{A}=\left({Z}{H}{A}\right){G}\left({Z}{H}{A}\right)$
16 14 15 syldan ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({Z}{G}{Z}\right){H}{A}=\left({Z}{H}{A}\right){G}\left({Z}{H}{A}\right)$
17 5 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {G}\in \mathrm{GrpOp}$
18 simpl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {R}\in \mathrm{RingOps}$
19 3 4 2 rngocl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {Z}\in {X}\wedge {A}\in {X}\right)\to {Z}{H}{A}\in {X}$
20 18 12 13 19 syl3anc ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {Z}{H}{A}\in {X}$
21 2 1 grporid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {Z}{H}{A}\in {X}\right)\to \left({Z}{H}{A}\right){G}{Z}={Z}{H}{A}$
22 21 eqcomd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {Z}{H}{A}\in {X}\right)\to {Z}{H}{A}=\left({Z}{H}{A}\right){G}{Z}$
23 17 20 22 syl2anc ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {Z}{H}{A}=\left({Z}{H}{A}\right){G}{Z}$
24 10 16 23 3eqtr3d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({Z}{H}{A}\right){G}\left({Z}{H}{A}\right)=\left({Z}{H}{A}\right){G}{Z}$
25 2 grpolcan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({Z}{H}{A}\in {X}\wedge {Z}\in {X}\wedge {Z}{H}{A}\in {X}\right)\right)\to \left(\left({Z}{H}{A}\right){G}\left({Z}{H}{A}\right)=\left({Z}{H}{A}\right){G}{Z}↔{Z}{H}{A}={Z}\right)$
26 17 20 12 20 25 syl13anc ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left(\left({Z}{H}{A}\right){G}\left({Z}{H}{A}\right)=\left({Z}{H}{A}\right){G}{Z}↔{Z}{H}{A}={Z}\right)$
27 24 26 mpbid ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {Z}{H}{A}={Z}$