rngsubdir

Description: Ring multiplication distributes over subtraction. ( subdir analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Hypotheses	ringsubdi.b	$⊢ B = {Base}_{R}$
	ringsubdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringsubdi.m	$⊢ \underset{˙}{-} = -_{R}$
	ringsubdi.r	$⊢ φ \to R \in Ring$
	ringsubdi.x	$⊢ φ \to X \in B$
	ringsubdi.y	$⊢ φ \to Y \in B$
	ringsubdi.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		ringsubdi.b	$⊢ B = {Base}_{R}$
2		ringsubdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringsubdi.m	$⊢ \underset{˙}{-} = -_{R}$
4		ringsubdi.r	$⊢ φ \to R \in Ring$
5		ringsubdi.x	$⊢ φ \to X \in B$
6		ringsubdi.y	$⊢ φ \to Y \in B$
7		ringsubdi.z	$⊢ φ \to Z \in B$
8		ringgrp	$⊢ R \in Ring \to R \in Grp$
9	4 8	syl	$⊢ φ \to R \in Grp$
10		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
11	1 10	grpinvcl	$⊢ (R \in Grp \land Y \in B) \to {inv}_{g} (R) (Y) \in B$
12	9 6 11	syl2anc	$⊢ φ \to {inv}_{g} (R) (Y) \in B$
13		eqid	$⊢ +_{R} = +_{R}$
14	1 13 2	ringdir	$⊢ (R \in Ring \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)$
15	4 5 12 7 14	syl13anc	$⊢ φ \to (X +_{R} {inv}_{g} (R) (Y)) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) +_{R} ({inv}_{g} (R) (Y) \underset{˙}{\cdot} Z)$
16	1 2 10 4 6 7	ringmneg1	$⊢ φ \to {inv}_{g} (R) (Y) \underset{˙}{\cdot} Z = {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
17	16	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)$
18	15 17	eqtrd	$⊢ φ \to (X +_{R} {inv}_{g} (R) (Y)) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) +_{R} {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
19	1 13 10 3	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{R} {inv}_{g} (R) (Y)$
20	5 6 19	syl2anc	$⊢ φ \to X \underset{˙}{-} Y = X +_{R} {inv}_{g} (R) (Y)$
21	20	oveq1d	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{\cdot} Z = (X +_{R} {inv}_{g} (R) (Y)) \underset{˙}{\cdot} Z$
22	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z \in B$
23	4 5 7 22	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Z \in B$
24	1 2	ringcl	$⊢ (R \in Ring \land Y \in B \land Z \in B) \to Y \underset{˙}{\cdot} Z \in B$
25	4 6 7 24	syl3anc	$⊢ φ \to Y \underset{˙}{\cdot} Z \in B$
26	1 13 10 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)$
27	23 25 26	syl2anc	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z) = (X \underset{˙}{\cdot} Z) +_{R} {inv}_{g} (R) (Y \underset{˙}{\cdot} Z)$
28	18 21 27	3eqtr4d	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{-} (Y \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem rngsubdir

Proof