This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvreq1

Description: Equality in terms of ratio equal to ring unity. ( diveq1 analog.) (Contributed by Mario Carneiro, 28-Apr-2016)

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

Proof

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