dvrass

Description: An associative law for division. ( divass analog.) (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	dvrass.b	$⊢ B = {Base}_{R}$
	dvrass.o	$⊢ U = Unit (R)$
	dvrass.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
	dvrass.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	dvrass	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Z = X \underset{˙}{\cdot} (Y \underset{˙}{\times} Z)$

Proof

Step	Hyp	Ref	Expression
1		dvrass.b	$⊢ B = {Base}_{R}$
2		dvrass.o	$⊢ U = Unit (R)$
3		dvrass.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
4		dvrass.t	$⊢ \underset{˙}{\cdot} = \cdot_{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		simpr3	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to Z \in U$
9		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
10	2 9 1	ringinvcl	$⊢ (R \in Ring \land Z \in U) \to {inv}_{r} (R) (Z) \in B$
11	5 8 10	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to {inv}_{r} (R) (Z) \in B$
12	1 4	ringass	$⊢ (R \in Ring \land (X \in B \land Y \in B \land {inv}_{r} (R) (Z) \in B)) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} {inv}_{r} (R) (Z) = X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} {inv}_{r} (R) (Z))$
13	5 6 7 11 12	syl13anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} {inv}_{r} (R) (Z) = X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} {inv}_{r} (R) (Z))$
14	1 4	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
15	14	3adant3r3	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to X \underset{˙}{\cdot} Y \in B$
16	1 4 2 9 3	dvrval	$⊢ (X \underset{˙}{\cdot} Y \in B \land Z \in U) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Z = (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} {inv}_{r} (R) (Z)$
17	15 8 16	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Z = (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} {inv}_{r} (R) (Z)$
18	1 4 2 9 3	dvrval	$⊢ (Y \in B \land Z \in U) \to Y \underset{˙}{\times} Z = Y \underset{˙}{\cdot} {inv}_{r} (R) (Z)$
19	7 8 18	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to Y \underset{˙}{\times} Z = Y \underset{˙}{\cdot} {inv}_{r} (R) (Z)$
20	19	oveq2d	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to X \underset{˙}{\cdot} (Y \underset{˙}{\times} Z) = X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} {inv}_{r} (R) (Z))$
21	13 17 20	3eqtr4d	$⊢ (R \in Ring \land (X \in B \land Y \in B \land Z \in U)) \to (X \underset{˙}{\cdot} Y) \underset{˙}{\times} Z = X \underset{˙}{\cdot} (Y \underset{˙}{\times} Z)$

Metamath Proof Explorer

Theorem dvrass

Proof