Theorem dvdsrspss

Description: In a ring, an element X divides Y iff the ideal generated by Y is a subset of the ideal generated by X (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	dvdsrspss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvdsrspss.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	dvdsrspss.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
	dvdsrspss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	dvdsrspss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	dvdsrspss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	dvdsrspss	⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsrspss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvdsrspss.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		dvdsrspss.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		dvdsrspss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		dvdsrspss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		dvdsrspss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8	1 3 7	dvdsr	⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) )
9	4	biantrurd	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) ) )
10	8 9	bitr4id	⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) )
11	1 7 2	elrspsn	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑡 ∈ 𝐵 𝑌 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) ) )
12	6 4 11	syl2anc	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑡 ∈ 𝐵 𝑌 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) ) )
13		eqcom	⊢ ( ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ↔ 𝑌 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) )
14	13	rexbii	⊢ ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ↔ ∃ 𝑡 ∈ 𝐵 𝑌 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) )
15	12 14	bitr4di	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑡 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑌 ) )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → 𝑅 ∈ Ring )
17	4	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
18		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
19	2 1 18	rspcl	⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑋 } ⊆ 𝐵 ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
20	6 17 19	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) )
23	22	snssd	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → { 𝑌 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
24	2 18	rspssp	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) ∧ { 𝑌 } ⊆ ( 𝐾 ‘ { 𝑋 } ) ) → ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) )
25	16 21 23 24	syl3anc	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) )
26		simpr	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) → ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) )
27	5	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ 𝐵 )
28	2 1	rspssid	⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑌 } ⊆ 𝐵 ) → { 𝑌 } ⊆ ( 𝐾 ‘ { 𝑌 } ) )
29	6 27 28	syl2anc	⊢ ( 𝜑 → { 𝑌 } ⊆ ( 𝐾 ‘ { 𝑌 } ) )
30		snssg	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑌 } ) ↔ { 𝑌 } ⊆ ( 𝐾 ‘ { 𝑌 } ) ) )
31	30	biimpar	⊢ ( ( 𝑌 ∈ 𝐵 ∧ { 𝑌 } ⊆ ( 𝐾 ‘ { 𝑌 } ) ) → 𝑌 ∈ ( 𝐾 ‘ { 𝑌 } ) )
32	5 29 31	syl2anc	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐾 ‘ { 𝑌 } ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) → 𝑌 ∈ ( 𝐾 ‘ { 𝑌 } ) )
34	26 33	sseldd	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) → 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) )
35	25 34	impbida	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
36	10 15 35	3bitr2d	⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )