rngsubdir

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

	Ref	Expression
Hypotheses	rngsubdi.b	$⊢ B = {Base}_{R}$
	rngsubdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rngsubdi.m	$⊢ \underset{˙}{-} = -_{R}$
	rngsubdi.r	$⊢ φ \to R \in Rng$
	rngsubdi.x	$⊢ φ \to X \in B$
	rngsubdi.y	$⊢ φ \to Y \in B$
	rngsubdi.z	$⊢ φ \to Z \in B$
Assertion	rngsubdir	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z)$

Proof

Step	Hyp	Ref	Expression
1		rngsubdi.b	$⊢ B = {Base}_{R}$
2		rngsubdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		rngsubdi.m	$⊢ \underset{˙}{-} = -_{R}$
4		rngsubdi.r	$⊢ φ \to R \in Rng$
5		rngsubdi.x	$⊢ φ \to X \in B$
6		rngsubdi.y	$⊢ φ \to Y \in B$
7		rngsubdi.z	$⊢ φ \to Z \in B$
8		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
9		rnggrp	$⊢ R \in Rng \to R \in Grp$
10	4 9	syl	$⊢ φ \to R \in Grp$
11	1 8 10 6	grpinvcld	$⊢ φ \to {inv}_{g} (R) (Y) \in B$
12		eqid	$⊢ +_{R} = +_{R}$
13	1 12 2	rngdir	$⊢ (R \in Rng \land (X \in B \land {inv}_{g} (R) (Y) \in B \land Z \in B)) \to (X +_{R} {inv}_{g} (R) (Y)) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) +_{R} ({inv}_{g} (R) (Y) \underset{˙}{\cdot} Z)$
14	4 5 11 7 13	syl13anc	$⊢ φ \to (X +_{R} {inv}_{g} (R) (Y)) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) +_{R} ({inv}_{g} (R) (Y) \underset{˙}{\cdot} Z)$
15	1 2 8 4 6 7	rngmneg1	$⊢ φ \to {inv}_{g} (R) (Y) \underset{˙}{\cdot} Z = {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
16	15	oveq2d	$⊢ φ \to (X \underset{˙}{\cdot} Z) +_{R} ({inv}_{g} (R) (Y) \underset{˙}{\cdot} Z) = (X \underset{˙}{\cdot} Z) +_{R} {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
17	14 16	eqtrd	$⊢ φ \to (X +_{R} {inv}_{g} (R) (Y)) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) +_{R} {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
18	1 12 8 3	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{R} {inv}_{g} (R) (Y)$
19	5 6 18	syl2anc	$⊢ φ \to X \underset{˙}{-} Y = X +_{R} {inv}_{g} (R) (Y)$
20	19	oveq1d	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{\cdot} Z = (X +_{R} {inv}_{g} (R) (Y)) \underset{˙}{\cdot} Z$
21	1 2	rngcl	$⊢ (R \in Rng \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z \in B$
22	4 5 7 21	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Z \in B$
23	1 2	rngcl	$⊢ (R \in Rng \land Y \in B \land Z \in B) \to Y \underset{˙}{\cdot} Z \in B$
24	4 6 7 23	syl3anc	$⊢ φ \to Y \underset{˙}{\cdot} Z \in B$
25	1 12 8 3	grpsubval	$⊢ (X \underset{˙}{\cdot} Z \in B \land Y \underset{˙}{\cdot} Z \in B) \to (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z) = (X \underset{˙}{\cdot} Z) +_{R} {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
26	22 24 25	syl2anc	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z) = (X \underset{˙}{\cdot} Z) +_{R} {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
27	17 20 26	3eqtr4d	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem rngsubdir

Proof