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 ⊢ 𝑍 = ( GId ‘ 𝐺 )
ringlz.2 ⊢ 𝑋 = ran 𝐺
ringlz.3 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ringlz.4 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
Assertion rngorz ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐻 𝑍 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 ringlz.1 ⊢ 𝑍 = ( GId ‘ 𝐺 )
2 ringlz.2 ⊢ 𝑋 = ran 𝐺
3 ringlz.3 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
4 ringlz.4 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
5 3 rngogrpo ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
6 2 1 grpoidcl ⊢ ( 𝐺 ∈ GrpOp → 𝑍 ∈ 𝑋 )
7 2 1 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑍 ∈ 𝑋 ) → ( 𝑍 𝐺 𝑍 ) = 𝑍 )
8 5 6 7 syl2anc2 ⊢ ( 𝑅 ∈ RingOps → ( 𝑍 𝐺 𝑍 ) = 𝑍 )
9 8 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑍 𝐺 𝑍 ) = 𝑍 )
10 9 oveq2d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐻 ( 𝑍 𝐺 𝑍 ) ) = ( 𝐴 𝐻 𝑍 ) )
11 simpr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
12 3 2 1 rngo0cl ⊢ ( 𝑅 ∈ RingOps → 𝑍 ∈ 𝑋 )
13 12 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → 𝑍 ∈ 𝑋 )
14 11 13 13 3jca ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) )
15 3 4 2 rngodi ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) ) → ( 𝐴 𝐻 ( 𝑍 𝐺 𝑍 ) ) = ( ( 𝐴 𝐻 𝑍 ) 𝐺 ( 𝐴 𝐻 𝑍 ) ) )
16 14 15 syldan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐻 ( 𝑍 𝐺 𝑍 ) ) = ( ( 𝐴 𝐻 𝑍 ) 𝐺 ( 𝐴 𝐻 𝑍 ) ) )
17 5 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → 𝐺 ∈ GrpOp )
18 3 4 2 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( 𝐴 𝐻 𝑍 ) ∈ 𝑋 )
19 13 18 mpd3an3 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐻 𝑍 ) ∈ 𝑋 )
20 2 1 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐻 𝑍 ) ∈ 𝑋 ) → ( 𝑍 𝐺 ( 𝐴 𝐻 𝑍 ) ) = ( 𝐴 𝐻 𝑍 ) )
21 20 eqcomd ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐻 𝑍 ) ∈ 𝑋 ) → ( 𝐴 𝐻 𝑍 ) = ( 𝑍 𝐺 ( 𝐴 𝐻 𝑍 ) ) )
22 17 19 21 syl2anc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐻 𝑍 ) = ( 𝑍 𝐺 ( 𝐴 𝐻 𝑍 ) ) )
23 10 16 22 3eqtr3d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐻 𝑍 ) 𝐺 ( 𝐴 𝐻 𝑍 ) ) = ( 𝑍 𝐺 ( 𝐴 𝐻 𝑍 ) ) )
24 2 grporcan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 𝐻 𝑍 ) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ ( 𝐴 𝐻 𝑍 ) ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐻 𝑍 ) 𝐺 ( 𝐴 𝐻 𝑍 ) ) = ( 𝑍 𝐺 ( 𝐴 𝐻 𝑍 ) ) ↔ ( 𝐴 𝐻 𝑍 ) = 𝑍 ) )
25 17 19 13 19 24 syl13anc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝐴 𝐻 𝑍 ) 𝐺 ( 𝐴 𝐻 𝑍 ) ) = ( 𝑍 𝐺 ( 𝐴 𝐻 𝑍 ) ) ↔ ( 𝐴 𝐻 𝑍 ) = 𝑍 ) )
26 23 25 mpbid ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐻 𝑍 ) = 𝑍 )