Metamath Proof Explorer

Theorem rngorz

Description: The zero of a unital ring is a right-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 rngorz ⊢ R ∈ RingOps ∧ A ∈ X → A H Z = 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 oveq2d ⊢ R ∈ RingOps ∧ A ∈ X → A H Z G Z = A H Z
11 simpr ⊢ R ∈ RingOps ∧ A ∈ X → A ∈ X
12 3 2 1 rngo0cl ⊢ R ∈ RingOps → Z ∈ X
13 12 adantr ⊢ R ∈ RingOps ∧ A ∈ X → Z ∈ X
14 11 13 13 3jca ⊢ R ∈ RingOps ∧ A ∈ X → A ∈ X ∧ Z ∈ X ∧ Z ∈ X
15 3 4 2 rngodi ⊢ R ∈ RingOps ∧ A ∈ X ∧ Z ∈ X ∧ Z ∈ X → A H Z G Z = A H Z G A H Z
16 14 15 syldan ⊢ R ∈ RingOps ∧ A ∈ X → A H Z G Z = A H Z G A H Z
17 5 adantr ⊢ R ∈ RingOps ∧ A ∈ X → G ∈ GrpOp
18 3 4 2 rngocl ⊢ R ∈ RingOps ∧ A ∈ X ∧ Z ∈ X → A H Z ∈ X
19 13 18 mpd3an3 ⊢ R ∈ RingOps ∧ A ∈ X → A H Z ∈ X
20 2 1 grpolid ⊢ G ∈ GrpOp ∧ A H Z ∈ X → Z G A H Z = A H Z
21 20 eqcomd ⊢ G ∈ GrpOp ∧ A H Z ∈ X → A H Z = Z G A H Z
22 17 19 21 syl2anc ⊢ R ∈ RingOps ∧ A ∈ X → A H Z = Z G A H Z
23 10 16 22 3eqtr3d ⊢ R ∈ RingOps ∧ A ∈ X → A H Z G A H Z = Z G A H Z
24 2 grporcan ⊢ G ∈ GrpOp ∧ A H Z ∈ X ∧ Z ∈ X ∧ A H Z ∈ X → A H Z G A H Z = Z G A H Z ↔ A H Z = Z
25 17 19 13 19 24 syl13anc ⊢ R ∈ RingOps ∧ A ∈ X → A H Z G A H Z = Z G A H Z ↔ A H Z = Z
26 23 25 mpbid ⊢ R ∈ RingOps ∧ A ∈ X → A H Z = Z