dvrcan5

Description: Cancellation law for common factor in ratio. ( divcan5 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		dvrcan5.b	$⊢ B = {Base}_{R}$
2		dvrcan5.o	$⊢ U = Unit (R)$
3		dvrcan5.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
4		dvrcan5.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5	1 2	unitss	$⊢ U \subseteq B$
6		simpr3	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Z \in U$
7	5 6	sseldi	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Z \in B$
8	2 4	unitmulcl	$⊢ (R \in Ring \land Y \in U \land Z \in U) \to Y \underset{˙}{\cdot} Z \in U$
9	8	3adant3r1	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Y \underset{˙}{\cdot} Z \in U$
10		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
11	1 4 2 10 3	dvrval	$⊢ (Z \in B \land Y \underset{˙}{\cdot} Z \in U) \to Z \underset{˙}{\times} (Y \underset{˙}{\cdot} Z) = Z \underset{˙}{\cdot} {inv}_{r} (R) (Y \underset{˙}{\cdot} Z)$
12	7 9 11	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Z \underset{˙}{\times} (Y \underset{˙}{\cdot} Z) = Z \underset{˙}{\cdot} {inv}_{r} (R) (Y \underset{˙}{\cdot} Z)$
13		simpl	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to R \in Ring$
14		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} U = {mulGrp}_{R} ↾_{𝑠} U$
15	2 14	unitgrp	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} U \in Grp$
16	13 15	syl	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to {mulGrp}_{R} ↾_{𝑠} U \in Grp$
17		simpr2	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Y \in U$
18	2 14	unitgrpbas	$⊢ U = {Base}_{({mulGrp}_{R} ↾_{𝑠} U)}$
19	2	fvexi	$⊢ U \in V$
20		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
21	20 4	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
22	14 21	ressplusg	$⊢ U \in V \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} U)}$
23	19 22	ax-mp	$⊢ \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} U)}$
24	2 14 10	invrfval	$⊢ {inv}_{r} (R) = {inv}_{g} ({mulGrp}_{R} ↾_{𝑠} U)$
25	18 23 24	grpinvadd	$⊢ ({mulGrp}_{R} ↾_{𝑠} U \in Grp \land Y \in U \land Z \in U) \to {inv}_{r} (R) (Y \underset{˙}{\cdot} Z) = {inv}_{r} (R) (Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
26	25	oveq2d	$⊢ ({mulGrp}_{R} ↾_{𝑠} U \in Grp \land Y \in U \land Z \in U) \to Z \underset{˙}{\cdot} {inv}_{r} (R) (Y \underset{˙}{\cdot} Z) = Z \underset{˙}{\cdot} ({inv}_{r} (R) (Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
27	16 17 6 26	syl3anc	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Z \underset{˙}{\cdot} {inv}_{r} (R) (Y \underset{˙}{\cdot} Z) = Z \underset{˙}{\cdot} ({inv}_{r} (R) (Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
28		eqid	$⊢ 1_{R} = 1_{R}$
29	2 10 4 28	unitrinv	$⊢ (R \in Ring \land Z \in U) \to Z \underset{˙}{\cdot} {inv}_{r} (R) (Z) = 1_{R}$
30	29	oveq1d	$⊢ (R \in Ring \land Z \in U) \to (Z \underset{˙}{\cdot} {inv}_{r} (R) (Z)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = 1_{R} \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
31	30	3ad2antr3	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to (Z \underset{˙}{\cdot} {inv}_{r} (R) (Z)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = 1_{R} \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
32	2 10	unitinvcl	$⊢ (R \in Ring \land Z \in U) \to {inv}_{r} (R) (Z) \in U$
33	32	3ad2antr3	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to {inv}_{r} (R) (Z) \in U$
34	5 33	sseldi	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to {inv}_{r} (R) (Z) \in B$
35	2 10	unitinvcl	$⊢ (R \in Ring \land Y \in U) \to {inv}_{r} (R) (Y) \in U$
36	35	3ad2antr2	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to {inv}_{r} (R) (Y) \in U$
37	5 36	sseldi	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to {inv}_{r} (R) (Y) \in B$
38	1 4	ringass	$⊢ (R \in Ring \land (Z \in B \land {inv}_{r} (R) (Z) \in B \land {inv}_{r} (R) (Y) \in B)) \to (Z \underset{˙}{\cdot} {inv}_{r} (R) (Z)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = Z \underset{˙}{\cdot} ({inv}_{r} (R) (Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
39	13 7 34 37 38	syl13anc	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to (Z \underset{˙}{\cdot} {inv}_{r} (R) (Z)) \underset{˙}{\cdot} {inv}_{r} (R) (Y) = Z \underset{˙}{\cdot} ({inv}_{r} (R) (Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y))$
40	1 4 28	ringlidm	$⊢ (R \in Ring \land {inv}_{r} (R) (Y) \in B) \to 1_{R} \underset{˙}{\cdot} {inv}_{r} (R) (Y) = {inv}_{r} (R) (Y)$
41	13 37 40	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to 1_{R} \underset{˙}{\cdot} {inv}_{r} (R) (Y) = {inv}_{r} (R) (Y)$
42	31 39 41	3eqtr3d	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Z \underset{˙}{\cdot} ({inv}_{r} (R) (Z) \underset{˙}{\cdot} {inv}_{r} (R) (Y)) = {inv}_{r} (R) (Y)$
43	12 27 42	3eqtrd	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to Z \underset{˙}{\times} (Y \underset{˙}{\cdot} Z) = {inv}_{r} (R) (Y)$
44	43	oveq2d	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to X \underset{˙}{\cdot} (Z \underset{˙}{\times} (Y \underset{˙}{\cdot} Z)) = X \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
45		simpr1	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to X \in B$
46	1 2 3 4	dvrass	$⊢ (R \in Ring \land (X \in B \land Z \in B \land Y \underset{˙}{\cdot} Z \in U)) \to (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} Z) = X \underset{˙}{\cdot} (Z \underset{˙}{\times} (Y \underset{˙}{\cdot} Z))$
47	13 45 7 9 46	syl13anc	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} Z) = X \underset{˙}{\cdot} (Z \underset{˙}{\times} (Y \underset{˙}{\cdot} Z))$
48	1 4 2 10 3	dvrval	$⊢ (X \in B \land Y \in U) \to X \underset{˙}{\times} Y = X \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
49	45 17 48	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to X \underset{˙}{\times} Y = X \underset{˙}{\cdot} {inv}_{r} (R) (Y)$
50	44 47 49	3eqtr4d	$⊢ (R \in Ring \land (X \in B \land Y \in U \land Z \in U)) \to (X \underset{˙}{\cdot} Z) \underset{˙}{\times} (Y \underset{˙}{\cdot} Z) = X \underset{˙}{\times} Y$

Metamath Proof Explorer

Theorem dvrcan5

Proof