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