ringsubdi

Description: Ring multiplication distributes over subtraction. ( subdi 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	ringsubdi	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{-} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{-} (X \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 Z \in B) \to {inv}_{g} (R) (Z) \in B$
12	9 7 11	syl2anc	$⊢ φ \to {inv}_{g} (R) (Z) \in B$
13		eqid	$⊢ +_{R} = +_{R}$
14	1 13 2	ringdi	$⊢ (R \in Ring \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))$
15	4 5 6 12 14	syl13anc	$⊢ φ \to X \underset{˙}{\cdot} (Y +_{R} {inv}_{g} (R) (Z)) = (X \underset{˙}{\cdot} Y) +_{R} (X \underset{˙}{\cdot} {inv}_{g} (R) (Z))$
16	1 2 10 4 5 7	ringmneg2	$⊢ φ \to X \underset{˙}{\cdot} {inv}_{g} (R) (Z) = {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
17	16	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)$
18	15 17	eqtrd	$⊢ φ \to X \underset{˙}{\cdot} (Y +_{R} {inv}_{g} (R) (Z)) = (X \underset{˙}{\cdot} Y) +_{R} {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
19	1 13 10 3	grpsubval	$⊢ (Y \in B \land Z \in B) \to Y \underset{˙}{-} Z = Y +_{R} {inv}_{g} (R) (Z)$
20	6 7 19	syl2anc	$⊢ φ \to Y \underset{˙}{-} Z = Y +_{R} {inv}_{g} (R) (Z)$
21	20	oveq2d	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{-} Z) = X \underset{˙}{\cdot} (Y +_{R} {inv}_{g} (R) (Z))$
22	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
23	4 5 6 22	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
24	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z \in B$
25	4 5 7 24	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Z \in B$
26	1 13 10 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)$
27	23 25 26	syl2anc	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{-} (X \underset{˙}{\cdot} Z) = (X \underset{˙}{\cdot} Y) +_{R} {inv}_{g} (R) (X \underset{˙}{\cdot} Z)$
28	18 21 27	3eqtr4d	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{-} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{-} (X \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem ringsubdi

Proof