Theorem rngsubdir

Description: Ring multiplication distributes over subtraction. ( subdir analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014) Generalization of ringsubdir . (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	rngsubdir	⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) )

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 6	grpinvcld	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
12		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
13	1 12 2	rngdir	⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) · 𝑍 ) ) )
14	4 5 11 7 13	syl13anc	⊢ ( 𝜑 → ( ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) · 𝑍 ) ) )
15	1 2 8 4 6 7	rngmneg1	⊢ ( 𝜑 → ( ( ( 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	5 6 18	syl2anc	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) )
20	19	oveq1d	⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) · 𝑍 ) = ( ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑍 ) )
21	1 2	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
22	4 5 7 21	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
23	1 2	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
24	4 6 7 23	syl3anc	⊢ ( 𝜑 → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
25	1 12 8 3	grpsubval	⊢ ( ( ( 𝑋 · 𝑍 ) ∈ 𝐵 ∧ ( 𝑌 · 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
26	22 24 25	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
27	17 20 26	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) )