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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )