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=GId⁡G
ringlz.2 ⊢X=ran⁡G
ringlz.3 ⊢G=1st⁡R
ringlz.4 ⊢H=2nd⁡R
Assertion rngolz ⊢R∈RingOps∧A∈X→ZHA=Z

Proof

Step Hyp Ref Expression
1 ringlz.1 ⊢Z=GId⁡G
2 ringlz.2 ⊢X=ran⁡G
3 ringlz.3 ⊢G=1st⁡R
4 ringlz.4 ⊢H=2nd⁡R
5 3 rngogrpo ⊢R∈RingOps→G∈GrpOp
6 2 1 grpoidcl ⊢G∈GrpOp→Z∈X
7 2 1 grpolid ⊢G∈GrpOp∧Z∈X→ZGZ=Z
8 5 6 7 syl2anc2 ⊢R∈RingOps→ZGZ=Z
9 8 adantr ⊢R∈RingOps∧A∈X→ZGZ=Z
10 9 oveq1d ⊢R∈RingOps∧A∈X→ZGZHA=ZHA
11 3 2 1 rngo0cl ⊢R∈RingOps→Z∈X
12 11 adantr ⊢R∈RingOps∧A∈X→Z∈X
13 simpr ⊢R∈RingOps∧A∈X→A∈X
14 12 12 13 3jca ⊢R∈RingOps∧A∈X→Z∈X∧Z∈X∧A∈X
15 3 4 2 rngodir ⊢R∈RingOps∧Z∈X∧Z∈X∧A∈X→ZGZHA=ZHAGZHA
16 14 15 syldan ⊢R∈RingOps∧A∈X→ZGZHA=ZHAGZHA
17 5 adantr ⊢R∈RingOps∧A∈X→G∈GrpOp
18 simpl ⊢R∈RingOps∧A∈X→R∈RingOps
19 3 4 2 rngocl ⊢R∈RingOps∧Z∈X∧A∈X→ZHA∈X
20 18 12 13 19 syl3anc ⊢R∈RingOps∧A∈X→ZHA∈X
21 2 1 grporid ⊢G∈GrpOp∧ZHA∈X→ZHAGZ=ZHA
22 21 eqcomd ⊢G∈GrpOp∧ZHA∈X→ZHA=ZHAGZ
23 17 20 22 syl2anc ⊢R∈RingOps∧A∈X→ZHA=ZHAGZ
24 10 16 23 3eqtr3d ⊢R∈RingOps∧A∈X→ZHAGZHA=ZHAGZ
25 2 grpolcan ⊢G∈GrpOp∧ZHA∈X∧Z∈X∧ZHA∈X→ZHAGZHA=ZHAGZ↔ZHA=Z
26 17 20 12 20 25 syl13anc ⊢R∈RingOps∧A∈X→ZHAGZHA=ZHAGZ↔ZHA=Z
27 24 26 mpbid ⊢R∈RingOps∧A∈X→ZHA=Z