Metamath Proof Explorer

Theorem ringlz

Description: The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009)

Ref Expression
Hypotheses ringz.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringz.t ⊢ · = ( .r ‘ 𝑅 )
ringz.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion ringlz ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = 0 )

Proof

Step Hyp Ref Expression
1 ringz.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringz.t ⊢ · = ( .r ‘ 𝑅 )
3 ringz.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
5 1 3 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
6 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
7 1 6 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ 0 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
8 4 5 7 syl2anc2 ⊢ ( 𝑅 ∈ Ring → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
9 8 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
10 9 oveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( 0 · 𝑋 ) )
11 4 5 syl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
12 11 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
13 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
14 12 12 13 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
15 1 6 2 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) )
16 14 15 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) )
17 4 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Grp )
18 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
19 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) ∈ 𝐵 )
20 18 12 13 19 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) ∈ 𝐵 )
21 1 6 3 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) → ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) = ( 0 · 𝑋 ) )
22 21 eqcomd ⊢ ( ( 𝑅 ∈ Grp ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
23 17 20 22 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
24 10 16 23 3eqtr3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
25 1 6 grplcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 0 · 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) ) → ( ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) ↔ ( 0 · 𝑋 ) = 0 ) )
26 17 20 12 20 25 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) ↔ ( 0 · 𝑋 ) = 0 ) )
27 24 26 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = 0 )