Theorem rngsubdi

Description: Ring multiplication distributes over subtraction. ( subdi analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014) ringsubdi generalized for non-unital rings. (Revised by AV, 23-Feb-2025)

	Ref	Expression
Hypotheses	rngsubdi.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rngsubdi.t	⊢ · = ( .r ‘ 𝑅 )
	rngsubdi.m	⊢ − = ( -g ‘ 𝑅 )
	rngsubdi.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rngsubdi.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	rngsubdi.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	rngsubdi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	rngsubdi	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 − 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) − ( 𝑋 · 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngsubdi.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rngsubdi.t	⊢ · = ( .r ‘ 𝑅 )
3		rngsubdi.m	⊢ − = ( -g ‘ 𝑅 )
4		rngsubdi.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
5		rngsubdi.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		rngsubdi.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		rngsubdi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
9		rnggrp	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
10	4 9	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
11	1 8 10 7	grpinvcld	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
12		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
13	1 12 2	rngdi	⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 ) ) → ( 𝑋 · ( 𝑌 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 · ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
14	4 5 6 11 13	syl13anc	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 · ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
15	1 2 8 4 5 7	rngmneg2	⊢ ( 𝜑 → ( 𝑋 · ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝑋 · 𝑍 ) ) )
16	15	oveq2d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 · ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑋 · 𝑍 ) ) ) )
17	14 16	eqtrd	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑋 · 𝑍 ) ) ) )
18	1 12 8 3	grpsubval	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 − 𝑍 ) = ( 𝑌 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) )
19	6 7 18	syl2anc	⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑌 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) )
20	19	oveq2d	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 − 𝑍 ) ) = ( 𝑋 · ( 𝑌 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
21	1 2	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
22	4 5 6 21	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
23	1 2	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
24	4 5 7 23	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
25	1 12 8 3	grpsubval	⊢ ( ( ( 𝑋 · 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) − ( 𝑋 · 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑋 · 𝑍 ) ) ) )
26	22 24 25	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) − ( 𝑋 · 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑋 · 𝑍 ) ) ) )
27	17 20 26	3eqtr4d	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 − 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) − ( 𝑋 · 𝑍 ) ) )