Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvdsrspss.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	dvdsrspss.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
	dvdsrspss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	dvdsrspss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	dvdsruassoi.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	dvdsruassoi.2	⊢ · = ( .r ‘ 𝑅 )
	dvdsruassoi.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	dvdsruassoi.3	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
	dvdsruassoi.4	⊢ ( 𝜑 → ( 𝑉 · 𝑋 ) = 𝑌 )
Assertion	dvdsruassoi	⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsrspss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvdsrspss.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		dvdsrspss.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		dvdsrspss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		dvdsrspss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		dvdsruassoi.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
7		dvdsruassoi.2	⊢ · = ( .r ‘ 𝑅 )
8		dvdsruassoi.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
9		dvdsruassoi.3	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
10		dvdsruassoi.4	⊢ ( 𝜑 → ( 𝑉 · 𝑋 ) = 𝑌 )
11	1 6	unitss	⊢ 𝑈 ⊆ 𝐵
12	11 9	sselid	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
13		oveq1	⊢ ( 𝑡 = 𝑉 → ( 𝑡 · 𝑋 ) = ( 𝑉 · 𝑋 ) )
14	13	eqeq1d	⊢ ( 𝑡 = 𝑉 → ( ( 𝑡 · 𝑋 ) = 𝑌 ↔ ( 𝑉 · 𝑋 ) = 𝑌 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑡 = 𝑉 ) → ( ( 𝑡 · 𝑋 ) = 𝑌 ↔ ( 𝑉 · 𝑋 ) = 𝑌 ) )
16	12 15 10	rspcedvd	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 )
17		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
18	6 17 1	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) ∈ 𝐵 )
19	8 9 18	syl2anc	⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) ∈ 𝐵 )
20		oveq1	⊢ ( 𝑠 = ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) → ( 𝑠 · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) )
21	20	eqeq1d	⊢ ( 𝑠 = ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) → ( ( 𝑠 · 𝑌 ) = 𝑋 ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) = 𝑋 ) )
22	21	adantl	⊢ ( ( 𝜑 ∧ 𝑠 = ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) ) → ( ( 𝑠 · 𝑌 ) = 𝑋 ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) = 𝑋 ) )
23	1 7 8 19 12 4	ringassd	⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · ( 𝑉 · 𝑋 ) ) )
24		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
25	6 17 7 24	unitlinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) = ( 1r ‘ 𝑅 ) )
26	8 9 25	syl2anc	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) = ( 1r ‘ 𝑅 ) )
27	26	oveq1d	⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
28	1 7 24 8 4	ringlidmd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
29	27 28	eqtrd	⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) · 𝑋 ) = 𝑋 )
30	10	oveq2d	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · ( 𝑉 · 𝑋 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) )
31	23 29 30	3eqtr3rd	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) = 𝑋 )
32	19 22 31	rspcedvd	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 )
33	1 3 7	dvdsr	⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) )
34	4	biantrurd	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) ) )
35	33 34	bitr4id	⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) )
36	1 3 7	dvdsr	⊢ ( 𝑌 ∥ 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) )
37	5	biantrurd	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) ) )
38	36 37	bitr4id	⊢ ( 𝜑 → ( 𝑌 ∥ 𝑋 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) )
39	35 38	anbi12d	⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) ) )
40	16 32 39	mpbir2and	⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) )