dvrdir

Description: Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017)

	Ref	Expression
Hypotheses	dvrdir.b	$⊢ B = {Base}_{R}$
	dvrdir.u	$⊢ U = Unit (R)$
	dvrdir.p	$⊢ \underset{˙}{+} = +_{R}$
	dvrdir.t	$⊢ \underset{˙}{\times} = /_{r} (R)$
Assertion	dvrdir	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \underset{˙}{\times} Z)$

Proof

Step	Hyp	Ref	Expression
1		dvrdir.b	$⊢ B = {Base}_{R}$
2		dvrdir.u	$⊢ U = Unit (R)$
3		dvrdir.p	$⊢ \underset{˙}{+} = +_{R}$
4		dvrdir.t	$⊢ \underset{˙}{\times} = /_{r} (R)$
5		simpl	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to R \in Ring$
6		simpr1	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to X \in B$
7		simpr2	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to Y \in B$
8	1 2	unitss	$⊢ U \subseteq B$
9		simpr3	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to Z \in U$
10		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
11	2 10	unitinvcl	$⊢ (R \in Ring \land Z \in U) \to {inv}_{r} (R) (Z) \in U$
12	9 11	syldan	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to {inv}_{r} (R) (Z) \in U$
13	8 12	sseldi	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to {inv}_{r} (R) (Z) \in B$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
15	1 3 14	ringdir	$⊢ (R \in Ring \land (X \in B \land Y \in B \land {inv}_{r} (R) (Z) \in B)) \to (X \underset{˙}{+} Y) \cdot_{R} {inv}_{r} (R) (Z) = (X \cdot_{R} {inv}_{r} (R) (Z)) \underset{˙}{+} (Y \cdot_{R} {inv}_{r} (R) (Z))$
16	5 6 7 13 15	syl13anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{+} Y) \cdot_{R} {inv}_{r} (R) (Z) = (X \cdot_{R} {inv}_{r} (R) (Z)) \underset{˙}{+} (Y \cdot_{R} {inv}_{r} (R) (Z))$
17		ringgrp	$⊢ R \in Ring \to R \in Grp$
18	17	adantr	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to R \in Grp$
19	1 3	grpcl	$⊢ (R \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
20	18 6 7 19	syl3anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to X \underset{˙}{+} Y \in B$
21	1 14 2 10 4	dvrval	$⊢ (X \underset{˙}{+} Y \in B \land Z \in U) \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (X \underset{˙}{+} Y) \cdot_{R} {inv}_{r} (R) (Z)$
22	20 9 21	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (X \underset{˙}{+} Y) \cdot_{R} {inv}_{r} (R) (Z)$
23	1 14 2 10 4	dvrval	$⊢ (X \in B \land Z \in U) \to X \underset{˙}{\times} Z = X \cdot_{R} {inv}_{r} (R) (Z)$
24	6 9 23	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to X \underset{˙}{\times} Z = X \cdot_{R} {inv}_{r} (R) (Z)$
25	1 14 2 10 4	dvrval	$⊢ (Y \in B \land Z \in U) \to Y \underset{˙}{\times} Z = Y \cdot_{R} {inv}_{r} (R) (Z)$
26	7 9 25	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to Y \underset{˙}{\times} Z = Y \cdot_{R} {inv}_{r} (R) (Z)$
27	24 26	oveq12d	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \underset{˙}{\times} Z) = (X \cdot_{R} {inv}_{r} (R) (Z)) \underset{˙}{+} (Y \cdot_{R} {inv}_{r} (R) (Z))$
28	16 22 27	3eqtr4d	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \underset{˙}{\times} Z)$

Metamath Proof Explorer

Theorem dvrdir

Proof