dvdsruasso

Description: Two elements X and Y of a ring R are associates, i.e. each divides the other, iff they are unit multiples of each 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}$
	dvdsruasso.r	$⊢ φ \to R \in IDomn$
Assertion	dvdsruasso	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow \exists u \in U u \underset{˙}{\cdot} X = Y)$

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		dvdsruasso.r	$⊢ φ \to R \in IDomn$
9	1 3 7	dvdsr	$⊢ X \underset{˙}{∥} Y \leftrightarrow (X \in B \land \exists t \in B t \underset{˙}{\cdot} X = Y)$
10	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))$
11	9 10	bitr4id	$⊢ φ \to (X \underset{˙}{∥} Y \leftrightarrow \exists t \in B t \underset{˙}{\cdot} X = Y)$
12	1 3 7	dvdsr	$⊢ Y \underset{˙}{∥} X \leftrightarrow (Y \in B \land \exists s \in B s \underset{˙}{\cdot} Y = X)$
13	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))$
14	12 13	bitr4id	$⊢ φ \to (Y \underset{˙}{∥} X \leftrightarrow \exists s \in B s \underset{˙}{\cdot} Y = X)$
15	11 14	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))$
16	8	idomringd	$⊢ φ \to R \in Ring$
17		eqid	$⊢ 1_{R} = 1_{R}$
18	6 17	1unit	$⊢ R \in Ring \to 1_{R} \in U$
19	16 18	syl	$⊢ φ \to 1_{R} \in U$
20	19	ad5antr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to 1_{R} \in U$
21		oveq1	$⊢ u = 1_{R} \to u \underset{˙}{\cdot} X = 1_{R} \underset{˙}{\cdot} X$
22	21	eqeq1d	$⊢ u = 1_{R} \to (u \underset{˙}{\cdot} X = Y \leftrightarrow 1_{R} \underset{˙}{\cdot} X = Y)$
23	22	adantl	$⊢ ((((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \land u = 1_{R}) \to (u \underset{˙}{\cdot} X = Y \leftrightarrow 1_{R} \underset{˙}{\cdot} X = Y)$
24	16	ad5antr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to R \in Ring$
25	4	ad5antr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to X \in B$
26	1 7 17 24 25	ringlidmd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to 1_{R} \underset{˙}{\cdot} X = X$
27		simpr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to X = 0_{R}$
28	27	oveq2d	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to t \underset{˙}{\cdot} X = t \underset{˙}{\cdot} 0_{R}$
29		simplr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to t \underset{˙}{\cdot} X = Y$
30		simpllr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to t \in B$
31		eqid	$⊢ 0_{R} = 0_{R}$
32	1 7 31	ringrz	$⊢ (R \in Ring \land t \in B) \to t \underset{˙}{\cdot} 0_{R} = 0_{R}$
33	24 30 32	syl2anc	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to t \underset{˙}{\cdot} 0_{R} = 0_{R}$
34	28 29 33	3eqtr3rd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to 0_{R} = Y$
35	26 27 34	3eqtrd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to 1_{R} \underset{˙}{\cdot} X = Y$
36	20 23 35	rspcedvd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X = 0_{R}) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
37		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
38	8 37	sylib	$⊢ φ \to (R \in CRing \land R \in Domn)$
39	38	simpld	$⊢ φ \to R \in CRing$
40	39	ad5antr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to R \in CRing$
41		simp-5r	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to s \in B$
42		simpllr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to t \in B$
43	16	ad5antr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to R \in Ring$
44	1 7 43 41 42	ringcld	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to s \underset{˙}{\cdot} t \in B$
45	1 17	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
46	43 45	syl	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to 1_{R} \in B$
47	4	ad5antr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to X \in B$
48		simpr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to X \neq 0_{R}$
49		eldifsn	$⊢ X \in (B ∖ \{0_{R}\}) \leftrightarrow (X \in B \land X \neq 0_{R})$
50	47 48 49	sylanbrc	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to X \in (B ∖ \{0_{R}\})$
51	8	ad5antr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to R \in IDomn$
52		simplr	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to t \underset{˙}{\cdot} X = Y$
53	52	oveq2d	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to s \underset{˙}{\cdot} (t \underset{˙}{\cdot} X) = s \underset{˙}{\cdot} Y$
54		simp-4r	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to s \underset{˙}{\cdot} Y = X$
55	53 54	eqtrd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to s \underset{˙}{\cdot} (t \underset{˙}{\cdot} X) = X$
56	1 7 43 41 42 47	ringassd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to (s \underset{˙}{\cdot} t) \underset{˙}{\cdot} X = s \underset{˙}{\cdot} (t \underset{˙}{\cdot} X)$
57	1 7 17 43 47	ringlidmd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to 1_{R} \underset{˙}{\cdot} X = X$
58	55 56 57	3eqtr4d	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to (s \underset{˙}{\cdot} t) \underset{˙}{\cdot} X = 1_{R} \underset{˙}{\cdot} X$
59	1 31 7 44 46 50 51 58	idomrcan	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to s \underset{˙}{\cdot} t = 1_{R}$
60	43 18	syl	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to 1_{R} \in U$
61	59 60	eqeltrd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to s \underset{˙}{\cdot} t \in U$
62	6 7 1	unitmulclb	$⊢ (R \in CRing \land s \in B \land t \in B) \to (s \underset{˙}{\cdot} t \in U \leftrightarrow (s \in U \land t \in U))$
63	62	simplbda	$⊢ ((R \in CRing \land s \in B \land t \in B) \land s \underset{˙}{\cdot} t \in U) \to t \in U$
64	40 41 42 61 63	syl31anc	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to t \in U$
65		oveq1	$⊢ u = t \to u \underset{˙}{\cdot} X = t \underset{˙}{\cdot} X$
66	65	eqeq1d	$⊢ u = t \to (u \underset{˙}{\cdot} X = Y \leftrightarrow t \underset{˙}{\cdot} X = Y)$
67	66	adantl	$⊢ ((((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \land u = t) \to (u \underset{˙}{\cdot} X = Y \leftrightarrow t \underset{˙}{\cdot} X = Y)$
68	64 67 52	rspcedvd	$⊢ (((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \land X \neq 0_{R}) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
69	36 68	pm2.61dane	$⊢ ((((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land t \in B) \land t \underset{˙}{\cdot} X = Y) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
70	69	r19.29an	$⊢ (((φ \land s \in B) \land s \underset{˙}{\cdot} Y = X) \land \exists t \in B t \underset{˙}{\cdot} X = Y) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
71	70	an32s	$⊢ (((φ \land s \in B) \land \exists t \in B t \underset{˙}{\cdot} X = Y) \land s \underset{˙}{\cdot} Y = X) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
72	71	ex	$⊢ ((φ \land s \in B) \land \exists t \in B t \underset{˙}{\cdot} X = Y) \to (s \underset{˙}{\cdot} Y = X \to \exists u \in U u \underset{˙}{\cdot} X = Y)$
73	72	an32s	$⊢ ((φ \land \exists t \in B t \underset{˙}{\cdot} X = Y) \land s \in B) \to (s \underset{˙}{\cdot} Y = X \to \exists u \in U u \underset{˙}{\cdot} X = Y)$
74	73	imp	$⊢ (((φ \land \exists t \in B t \underset{˙}{\cdot} X = Y) \land s \in B) \land s \underset{˙}{\cdot} Y = X) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
75	74	r19.29an	$⊢ ((φ \land \exists t \in B t \underset{˙}{\cdot} X = Y) \land \exists s \in B s \underset{˙}{\cdot} Y = X) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
76	75	anasss	$⊢ (φ \land (\exists t \in B t \underset{˙}{\cdot} X = Y \land \exists s \in B s \underset{˙}{\cdot} Y = X)) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
77	15 76	sylbida	$⊢ (φ \land (X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X)) \to \exists u \in U u \underset{˙}{\cdot} X = Y$
78	4	ad2antrr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to X \in B$
79	5	ad2antrr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to Y \in B$
80	16	ad2antrr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to R \in Ring$
81		simplr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to u \in U$
82		simpr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to u \underset{˙}{\cdot} X = Y$
83	1 2 3 78 79 6 7 80 81 82	dvdsruassoi	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to (X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X)$
84	83	r19.29an	$⊢ (φ \land \exists u \in U u \underset{˙}{\cdot} X = Y) \to (X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X)$
85	77 84	impbida	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow \exists u \in U u \underset{˙}{\cdot} X = Y)$

Metamath Proof Explorer

Theorem dvdsruasso

Proof