Theorem rnglz

Description: The zero of a non-unital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rngcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rngcl.t	⊢ · = ( .r ‘ 𝑅 )
3		rnglz.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		rngabl	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
5		ablgrp	⊢ ( 𝑅 ∈ Abel → 𝑅 ∈ Grp )
6	4 5	syl	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
7	1 3	grpidcl	⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
8		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9	1 8 3	grplid	⊢ ( ( 𝑅 ∈ Grp ∧ 0 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
10	6 7 9	syl2anc2	⊢ ( 𝑅 ∈ Rng → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
11	10	adantr	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
12	11	oveq1d	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( 0 · 𝑋 ) )
13		simpl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Rng )
14	6 7	syl	⊢ ( 𝑅 ∈ Rng → 0 ∈ 𝐵 )
15	14 14	jca	⊢ ( 𝑅 ∈ Rng → ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) )
16	15	anim1i	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) )
17		df-3an	⊢ ( ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ↔ ( ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) )
18	16 17	sylibr	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
19	1 8 2	rngdir	⊢ ( ( 𝑅 ∈ Rng ∧ ( 0 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) )
20	13 18 19	syl2anc	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 ( +g ‘ 𝑅 ) 0 ) · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) )
21	6	adantr	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Grp )
22	14	adantr	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
23		simpr	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
24	1 2	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) ∈ 𝐵 )
25	13 22 23 24	syl3anc	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) ∈ 𝐵 )
26	1 8 3	grprid	⊢ ( ( 𝑅 ∈ Grp ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) → ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) = ( 0 · 𝑋 ) )
27	26	eqcomd	⊢ ( ( 𝑅 ∈ Grp ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
28	21 25 27	syl2anc	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
29	12 20 28	3eqtr3d	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) )
30	1 8	grplcan	⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 0 · 𝑋 ) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ( 0 · 𝑋 ) ∈ 𝐵 ) ) → ( ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) ↔ ( 0 · 𝑋 ) = 0 ) )
31	21 25 22 25 30	syl13anc	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) ( 0 · 𝑋 ) ) = ( ( 0 · 𝑋 ) ( +g ‘ 𝑅 ) 0 ) ↔ ( 0 · 𝑋 ) = 0 ) )
32	29 31	mpbid	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = 0 )