Theorem dvreq1

Description: A cancellation law for division. ( diveq1 analog.) (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dvreq1.b	$$⊢B={\mathrm{Base}}_R$$
	dvreq1.o	$$⊢U=\mathrm{Unit}\left(R\right)$$
	dvreq1.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
	dvreq1.t	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	dvreq1	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to \left(X\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}\leftrightarrow X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvreq1.b	$$⊢B={\mathrm{Base}}_R$$
2		dvreq1.o	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		dvreq1.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
4		dvreq1.t	$$⊢\underset{\dot{}}{1}=1_R$$
5		oveq1	$$⊢X\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}\to \left(X\underset{\dot{}}{\times }Y\right){\cdot }_{R}Y=\underset{\dot{}}{1}{\cdot }_{R}Y$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7	1 2 3 6	dvrcan1	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to \left(X\underset{\dot{}}{\times }Y\right){\cdot }_{R}Y=X$$
8	1 2	unitcl	$$⊢Y\in U\to Y\in B$$
9	1 6 4	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to \underset{\dot{}}{1}{\cdot }_{R}Y=Y$$
10	8 9	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in U\right)\to \underset{\dot{}}{1}{\cdot }_{R}Y=Y$$
11	10	3adant2	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to \underset{\dot{}}{1}{\cdot }_{R}Y=Y$$
12	7 11	eqeq12d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to \left(\left(X\underset{\dot{}}{\times }Y\right){\cdot }_{R}Y=\underset{\dot{}}{1}{\cdot }_{R}Y\leftrightarrow X=Y\right)$$
13	5 12	syl5ib	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to \left(X\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}\to X=Y\right)$$
14	2 3 4	dvrid	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in U\right)\to Y\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}$$
15	14	3adant2	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to Y\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}$$
16		oveq1	$$⊢X=Y\to X\underset{\dot{}}{\times }Y=Y\underset{\dot{}}{\times }Y$$
17	16	eqeq1d	$$⊢X=Y\to \left(X\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}\leftrightarrow Y\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}\right)$$
18	15 17	syl5ibrcom	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to \left(X=Y\to X\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}\right)$$
19	13 18	impbid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in U\right)\to \left(X\underset{\dot{}}{\times }Y=\underset{\dot{}}{1}\leftrightarrow X=Y\right)$$