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 = 1 st R
ringlz.4 H = 2 nd R
Assertion rngolz R RingOps A X Z H A = Z

Proof

Step Hyp Ref Expression
1 ringlz.1 Z = GId G
2 ringlz.2 X = ran G
3 ringlz.3 G = 1 st R
4 ringlz.4 H = 2 nd R
5 3 rngogrpo R RingOps G GrpOp
6 2 1 grpoidcl G GrpOp Z X
7 2 1 grpolid G GrpOp Z X Z G Z = Z
8 5 6 7 syl2anc2 R RingOps Z G Z = Z
9 8 adantr R RingOps A X Z G Z = Z
10 9 oveq1d R RingOps A X Z G Z H A = Z H A
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 Z G Z H A = Z H A G Z H A
16 14 15 syldan R RingOps A X Z G Z H A = Z H A G Z H A
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 Z H A X
20 18 12 13 19 syl3anc R RingOps A X Z H A X
21 2 1 grporid G GrpOp Z H A X Z H A G Z = Z H A
22 21 eqcomd G GrpOp Z H A X Z H A = Z H A G Z
23 17 20 22 syl2anc R RingOps A X Z H A = Z H A G Z
24 10 16 23 3eqtr3d R RingOps A X Z H A G Z H A = Z H A G Z
25 2 grpolcan G GrpOp Z H A X Z X Z H A X Z H A G Z H A = Z H A G Z Z H A = Z
26 17 20 12 20 25 syl13anc R RingOps A X Z H A G Z H A = Z H A G Z Z H A = Z
27 24 26 mpbid R RingOps A X Z H A = Z