Theorem rngdir

Description: Distributive law for the multiplication operation of a nonunital ring (right-distributivity). (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	rngdi.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rngdi.p	⊢ + = ( +g ‘ 𝑅 )
	rngdi.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	rngdir	⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngdi.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rngdi.p	⊢ + = ( +g ‘ 𝑅 )
3		rngdi.t	⊢ · = ( .r ‘ 𝑅 )
4		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5	1 4 2 3	isrng	⊢ ( 𝑅 ∈ Rng ↔ ( 𝑅 ∈ Abel ∧ ( mulGrp ‘ 𝑅 ) ∈ Smgrp ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑐 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑐 ) = ( ( 𝑎 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) ) )
6		oveq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 · ( 𝑏 + 𝑐 ) ) = ( 𝑋 · ( 𝑏 + 𝑐 ) ) )
7		oveq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 · 𝑏 ) = ( 𝑋 · 𝑏 ) )
8		oveq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 · 𝑐 ) = ( 𝑋 · 𝑐 ) )
9	7 8	oveq12d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑐 ) ) = ( ( 𝑋 · 𝑏 ) + ( 𝑋 · 𝑐 ) ) )
10	6 9	eqeq12d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑐 ) ) ↔ ( 𝑋 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑋 · 𝑏 ) + ( 𝑋 · 𝑐 ) ) ) )
11		oveq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 + 𝑏 ) = ( 𝑋 + 𝑏 ) )
12	11	oveq1d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 + 𝑏 ) · 𝑐 ) = ( ( 𝑋 + 𝑏 ) · 𝑐 ) )
13	8	oveq1d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) = ( ( 𝑋 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) )
14	12 13	eqeq12d	⊢ ( 𝑎 = 𝑋 → ( ( ( 𝑎 + 𝑏 ) · 𝑐 ) = ( ( 𝑎 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ↔ ( ( 𝑋 + 𝑏 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) )
15	10 14	anbi12d	⊢ ( 𝑎 = 𝑋 → ( ( ( 𝑎 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑐 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑐 ) = ( ( 𝑎 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) ↔ ( ( 𝑋 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑋 · 𝑏 ) + ( 𝑋 · 𝑐 ) ) ∧ ( ( 𝑋 + 𝑏 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) ) )
16		oveq1	⊢ ( 𝑏 = 𝑌 → ( 𝑏 + 𝑐 ) = ( 𝑌 + 𝑐 ) )
17	16	oveq2d	⊢ ( 𝑏 = 𝑌 → ( 𝑋 · ( 𝑏 + 𝑐 ) ) = ( 𝑋 · ( 𝑌 + 𝑐 ) ) )
18		oveq2	⊢ ( 𝑏 = 𝑌 → ( 𝑋 · 𝑏 ) = ( 𝑋 · 𝑌 ) )
19	18	oveq1d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 · 𝑏 ) + ( 𝑋 · 𝑐 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑐 ) ) )
20	17 19	eqeq12d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑋 · 𝑏 ) + ( 𝑋 · 𝑐 ) ) ↔ ( 𝑋 · ( 𝑌 + 𝑐 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑐 ) ) ) )
21		oveq2	⊢ ( 𝑏 = 𝑌 → ( 𝑋 + 𝑏 ) = ( 𝑋 + 𝑌 ) )
22	21	oveq1d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 + 𝑏 ) · 𝑐 ) = ( ( 𝑋 + 𝑌 ) · 𝑐 ) )
23		oveq1	⊢ ( 𝑏 = 𝑌 → ( 𝑏 · 𝑐 ) = ( 𝑌 · 𝑐 ) )
24	23	oveq2d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) = ( ( 𝑋 · 𝑐 ) + ( 𝑌 · 𝑐 ) ) )
25	22 24	eqeq12d	⊢ ( 𝑏 = 𝑌 → ( ( ( 𝑋 + 𝑏 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ↔ ( ( 𝑋 + 𝑌 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑌 · 𝑐 ) ) ) )
26	20 25	anbi12d	⊢ ( 𝑏 = 𝑌 → ( ( ( 𝑋 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑋 · 𝑏 ) + ( 𝑋 · 𝑐 ) ) ∧ ( ( 𝑋 + 𝑏 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) ↔ ( ( 𝑋 · ( 𝑌 + 𝑐 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑐 ) ) ∧ ( ( 𝑋 + 𝑌 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑌 · 𝑐 ) ) ) ) )
27		oveq2	⊢ ( 𝑐 = 𝑍 → ( 𝑌 + 𝑐 ) = ( 𝑌 + 𝑍 ) )
28	27	oveq2d	⊢ ( 𝑐 = 𝑍 → ( 𝑋 · ( 𝑌 + 𝑐 ) ) = ( 𝑋 · ( 𝑌 + 𝑍 ) ) )
29		oveq2	⊢ ( 𝑐 = 𝑍 → ( 𝑋 · 𝑐 ) = ( 𝑋 · 𝑍 ) )
30	29	oveq2d	⊢ ( 𝑐 = 𝑍 → ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑐 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) )
31	28 30	eqeq12d	⊢ ( 𝑐 = 𝑍 → ( ( 𝑋 · ( 𝑌 + 𝑐 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑐 ) ) ↔ ( 𝑋 · ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) ) )
32		oveq2	⊢ ( 𝑐 = 𝑍 → ( ( 𝑋 + 𝑌 ) · 𝑐 ) = ( ( 𝑋 + 𝑌 ) · 𝑍 ) )
33		oveq2	⊢ ( 𝑐 = 𝑍 → ( 𝑌 · 𝑐 ) = ( 𝑌 · 𝑍 ) )
34	29 33	oveq12d	⊢ ( 𝑐 = 𝑍 → ( ( 𝑋 · 𝑐 ) + ( 𝑌 · 𝑐 ) ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) )
35	32 34	eqeq12d	⊢ ( 𝑐 = 𝑍 → ( ( ( 𝑋 + 𝑌 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑌 · 𝑐 ) ) ↔ ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) )
36	31 35	anbi12d	⊢ ( 𝑐 = 𝑍 → ( ( ( 𝑋 · ( 𝑌 + 𝑐 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑐 ) ) ∧ ( ( 𝑋 + 𝑌 ) · 𝑐 ) = ( ( 𝑋 · 𝑐 ) + ( 𝑌 · 𝑐 ) ) ) ↔ ( ( 𝑋 · ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) ∧ ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) ) )
37	15 26 36	rspc3v	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑐 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑐 ) = ( ( 𝑎 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) → ( ( 𝑋 · ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) ∧ ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) ) )
38		simpr	⊢ ( ( ( 𝑋 · ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) ∧ ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) )
39	37 38	syl6com	⊢ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑐 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑐 ) = ( ( 𝑎 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) )
40	39	3ad2ant3	⊢ ( ( 𝑅 ∈ Abel ∧ ( mulGrp ‘ 𝑅 ) ∈ Smgrp ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) + ( 𝑎 · 𝑐 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑐 ) = ( ( 𝑎 · 𝑐 ) + ( 𝑏 · 𝑐 ) ) ) ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) )
41	5 40	sylbi	⊢ ( 𝑅 ∈ Rng → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) )
42	41	imp	⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) )