rngsubdi

Description: Ring multiplication distributes over subtraction. ( subdi analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014) Generalization of ringsubdi . (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	rngsubdi	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{-} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{-} (X \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 7	grpinvcld	$⊢ φ \to {inv}_{g} (R) (Z) \in B$
12		eqid	$⊢ +_{R} = +_{R}$
13	1 12 2	rngdi	$⊢ (R \in Rng \land (X \in B \land Y \in B \land {inv}_{g} (R) (Z) \in B)) \to X \underset{˙}{\cdot} (Y +_{R} {inv}_{g} (R) (Z)) = (X \underset{˙}{\cdot} Y) +_{R} (X \underset{˙}{\cdot} {inv}_{g} (R) (Z))$
14	4 5 6 11 13	syl13anc	$⊢ φ \to X \underset{˙}{\cdot} (Y +_{R} {inv}_{g} (R) (Z)) = (X \underset{˙}{\cdot} Y) +_{R} (X \underset{˙}{\cdot} {inv}_{g} (R) (Z))$
15	1 2 8 4 5 7	rngmneg2	$⊢ φ \to X \underset{˙}{\cdot} {inv}_{g} (R) (Z) = {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
16	15	oveq2d	$⊢ φ \to (X \underset{˙}{\cdot} Y) +_{R} (X \underset{˙}{\cdot} {inv}_{g} (R) (Z)) = (X \underset{˙}{\cdot} Y) +_{R} {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
17	14 16	eqtrd	$⊢ φ \to X \underset{˙}{\cdot} (Y +_{R} {inv}_{g} (R) (Z)) = (X \underset{˙}{\cdot} Y) +_{R} {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
18	1 12 8 3	grpsubval	$⊢ (Y \in B \land Z \in B) \to Y \underset{˙}{-} Z = Y +_{R} {inv}_{g} (R) (Z)$
19	6 7 18	syl2anc	$⊢ φ \to Y \underset{˙}{-} Z = Y +_{R} {inv}_{g} (R) (Z)$
20	19	oveq2d	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{-} Z) = X \underset{˙}{\cdot} (Y +_{R} {inv}_{g} (R) (Z))$
21	1 2	rngcl	$⊢ (R \in Rng \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
22	4 5 6 21	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
23	1 2	rngcl	$⊢ (R \in Rng \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z \in B$
24	4 5 7 23	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Z \in B$
25	1 12 8 3	grpsubval	$⊢ (X \underset{˙}{\cdot} Y \in B \land X \underset{˙}{\cdot} Z \in B) \to (X \underset{˙}{\cdot} Y) \underset{˙}{-} (X \underset{˙}{\cdot} Z) = (X \underset{˙}{\cdot} Y) +_{R} {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
26	22 24 25	syl2anc	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{-} (X \underset{˙}{\cdot} Z) = (X \underset{˙}{\cdot} Y) +_{R} {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
27	17 20 26	3eqtr4d	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{-} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{-} (X \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem rngsubdi

Proof