dvdsruassoi

Description: If two elements X and Y of a ring R are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	dvdsrspss.b	$⊢ B = {Base}_{R}$
	dvdsrspss.k	$⊢ K = RSpan (R)$
	dvdsrspss.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	dvdsrspss.x	$⊢ φ \to X \in B$
	dvdsrspss.y	$⊢ φ \to Y \in B$
	dvdsruassoi.1	$⊢ U = Unit (R)$
	dvdsruassoi.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	dvdsruassoi.r	$⊢ φ \to R \in Ring$
	dvdsruassoi.3	$⊢ φ \to V \in U$
	dvdsruassoi.4	$⊢ φ \to V \underset{˙}{\cdot} X = Y$
Assertion	dvdsruassoi	$⊢ φ \to (X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X)$

Proof

Step	Hyp	Ref	Expression
1		dvdsrspss.b	$⊢ B = {Base}_{R}$
2		dvdsrspss.k	$⊢ K = RSpan (R)$
3		dvdsrspss.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
4		dvdsrspss.x	$⊢ φ \to X \in B$
5		dvdsrspss.y	$⊢ φ \to Y \in B$
6		dvdsruassoi.1	$⊢ U = Unit (R)$
7		dvdsruassoi.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		dvdsruassoi.r	$⊢ φ \to R \in Ring$
9		dvdsruassoi.3	$⊢ φ \to V \in U$
10		dvdsruassoi.4	$⊢ φ \to V \underset{˙}{\cdot} X = Y$
11	1 6	unitss	$⊢ U \subseteq B$
12	11 9	sselid	$⊢ φ \to V \in B$
13		oveq1	$⊢ t = V \to t \underset{˙}{\cdot} X = V \underset{˙}{\cdot} X$
14	13	eqeq1d	$⊢ t = V \to (t \underset{˙}{\cdot} X = Y \leftrightarrow V \underset{˙}{\cdot} X = Y)$
15	14	adantl	$⊢ (φ \land t = V) \to (t \underset{˙}{\cdot} X = Y \leftrightarrow V \underset{˙}{\cdot} X = Y)$
16	12 15 10	rspcedvd	$⊢ φ \to \exists t \in B t \underset{˙}{\cdot} X = Y$
17		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
18	6 17 1	ringinvcl	$⊢ (R \in Ring \land V \in U) \to {inv}_{r} (R) (V) \in B$
19	8 9 18	syl2anc	$⊢ φ \to {inv}_{r} (R) (V) \in B$
20		oveq1	$⊢ s = {inv}_{r} (R) (V) \to s \underset{˙}{\cdot} Y = {inv}_{r} (R) (V) \underset{˙}{\cdot} Y$
21	20	eqeq1d	$⊢ s = {inv}_{r} (R) (V) \to (s \underset{˙}{\cdot} Y = X \leftrightarrow {inv}_{r} (R) (V) \underset{˙}{\cdot} Y = X)$
22	21	adantl	$⊢ (φ \land s = {inv}_{r} (R) (V)) \to (s \underset{˙}{\cdot} Y = X \leftrightarrow {inv}_{r} (R) (V) \underset{˙}{\cdot} Y = X)$
23	1 7 8 19 12 4	ringassd	$⊢ φ \to ({inv}_{r} (R) (V) \underset{˙}{\cdot} V) \underset{˙}{\cdot} X = {inv}_{r} (R) (V) \underset{˙}{\cdot} (V \underset{˙}{\cdot} X)$
24		eqid	$⊢ 1_{R} = 1_{R}$
25	6 17 7 24	unitlinv	$⊢ (R \in Ring \land V \in U) \to {inv}_{r} (R) (V) \underset{˙}{\cdot} V = 1_{R}$
26	8 9 25	syl2anc	$⊢ φ \to {inv}_{r} (R) (V) \underset{˙}{\cdot} V = 1_{R}$
27	26	oveq1d	$⊢ φ \to ({inv}_{r} (R) (V) \underset{˙}{\cdot} V) \underset{˙}{\cdot} X = 1_{R} \underset{˙}{\cdot} X$
28	1 7 24 8 4	ringlidmd	$⊢ φ \to 1_{R} \underset{˙}{\cdot} X = X$
29	27 28	eqtrd	$⊢ φ \to ({inv}_{r} (R) (V) \underset{˙}{\cdot} V) \underset{˙}{\cdot} X = X$
30	10	oveq2d	$⊢ φ \to {inv}_{r} (R) (V) \underset{˙}{\cdot} (V \underset{˙}{\cdot} X) = {inv}_{r} (R) (V) \underset{˙}{\cdot} Y$
31	23 29 30	3eqtr3rd	$⊢ φ \to {inv}_{r} (R) (V) \underset{˙}{\cdot} Y = X$
32	19 22 31	rspcedvd	$⊢ φ \to \exists s \in B s \underset{˙}{\cdot} Y = X$
33	1 3 7	dvdsr	$⊢ X \underset{˙}{∥} Y \leftrightarrow (X \in B \land \exists t \in B t \underset{˙}{\cdot} X = Y)$
34	4	biantrurd	$⊢ φ \to (\exists t \in B t \underset{˙}{\cdot} X = Y \leftrightarrow (X \in B \land \exists t \in B t \underset{˙}{\cdot} X = Y))$
35	33 34	bitr4id	$⊢ φ \to (X \underset{˙}{∥} Y \leftrightarrow \exists t \in B t \underset{˙}{\cdot} X = Y)$
36	1 3 7	dvdsr	$⊢ Y \underset{˙}{∥} X \leftrightarrow (Y \in B \land \exists s \in B s \underset{˙}{\cdot} Y = X)$
37	5	biantrurd	$⊢ φ \to (\exists s \in B s \underset{˙}{\cdot} Y = X \leftrightarrow (Y \in B \land \exists s \in B s \underset{˙}{\cdot} Y = X))$
38	36 37	bitr4id	$⊢ φ \to (Y \underset{˙}{∥} X \leftrightarrow \exists s \in B s \underset{˙}{\cdot} Y = X)$
39	35 38	anbi12d	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow (\exists t \in B t \underset{˙}{\cdot} X = Y \land \exists s \in B s \underset{˙}{\cdot} Y = X))$
40	16 32 39	mpbir2and	$⊢ φ \to (X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X)$

Metamath Proof Explorer

Theorem dvdsruassoi

Proof