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 
|- B = ( Base ` R )
dvdsrspss.k 
|- K = ( RSpan ` R )
dvdsrspss.d 
|- .|| = ( ||r ` R )
dvdsrspss.x 
|- ( ph -> X e. B )
dvdsrspss.y 
|- ( ph -> Y e. B )
dvdsrspss.r 
|- ( ph -> R e. Ring )
Assertion dvdsrspss 
|- ( ph -> ( X .|| Y <-> ( K ` { Y } ) C_ ( K ` { X } ) ) )

Proof

Step Hyp Ref Expression
1 dvdsrspss.b 
 |-  B = ( Base ` R )
2 dvdsrspss.k 
 |-  K = ( RSpan ` R )
3 dvdsrspss.d 
 |-  .|| = ( ||r ` R )
4 dvdsrspss.x 
 |-  ( ph -> X e. B )
5 dvdsrspss.y 
 |-  ( ph -> Y e. B )
6 dvdsrspss.r 
 |-  ( ph -> R e. Ring )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 1 3 7 dvdsr 
 |-  ( X .|| Y <-> ( X e. B /\ E. t e. B ( t ( .r ` R ) X ) = Y ) )
9 4 biantrurd 
 |-  ( ph -> ( E. t e. B ( t ( .r ` R ) X ) = Y <-> ( X e. B /\ E. t e. B ( t ( .r ` R ) X ) = Y ) ) )
10 8 9 bitr4id 
 |-  ( ph -> ( X .|| Y <-> E. t e. B ( t ( .r ` R ) X ) = Y ) )
11 1 7 2 elrspsn 
 |-  ( ( R e. Ring /\ X e. B ) -> ( Y e. ( K ` { X } ) <-> E. t e. B Y = ( t ( .r ` R ) X ) ) )
12 6 4 11 syl2anc 
 |-  ( ph -> ( Y e. ( K ` { X } ) <-> E. t e. B Y = ( t ( .r ` R ) X ) ) )
13 eqcom 
 |-  ( ( t ( .r ` R ) X ) = Y <-> Y = ( t ( .r ` R ) X ) )
14 13 rexbii 
 |-  ( E. t e. B ( t ( .r ` R ) X ) = Y <-> E. t e. B Y = ( t ( .r ` R ) X ) )
15 12 14 bitr4di 
 |-  ( ph -> ( Y e. ( K ` { X } ) <-> E. t e. B ( t ( .r ` R ) X ) = Y ) )
16 6 adantr 
 |-  ( ( ph /\ Y e. ( K ` { X } ) ) -> R e. Ring )
17 4 snssd 
 |-  ( ph -> { X } C_ B )
18 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
19 2 1 18 rspcl 
 |-  ( ( R e. Ring /\ { X } C_ B ) -> ( K ` { X } ) e. ( LIdeal ` R ) )
20 6 17 19 syl2anc 
 |-  ( ph -> ( K ` { X } ) e. ( LIdeal ` R ) )
21 20 adantr 
 |-  ( ( ph /\ Y e. ( K ` { X } ) ) -> ( K ` { X } ) e. ( LIdeal ` R ) )
22 simpr 
 |-  ( ( ph /\ Y e. ( K ` { X } ) ) -> Y e. ( K ` { X } ) )
23 22 snssd 
 |-  ( ( ph /\ Y e. ( K ` { X } ) ) -> { Y } C_ ( K ` { X } ) )
24 2 18 rspssp 
 |-  ( ( R e. Ring /\ ( K ` { X } ) e. ( LIdeal ` R ) /\ { Y } C_ ( K ` { X } ) ) -> ( K ` { Y } ) C_ ( K ` { X } ) )
25 16 21 23 24 syl3anc 
 |-  ( ( ph /\ Y e. ( K ` { X } ) ) -> ( K ` { Y } ) C_ ( K ` { X } ) )
26 simpr 
 |-  ( ( ph /\ ( K ` { Y } ) C_ ( K ` { X } ) ) -> ( K ` { Y } ) C_ ( K ` { X } ) )
27 5 snssd 
 |-  ( ph -> { Y } C_ B )
28 2 1 rspssid 
 |-  ( ( R e. Ring /\ { Y } C_ B ) -> { Y } C_ ( K ` { Y } ) )
29 6 27 28 syl2anc 
 |-  ( ph -> { Y } C_ ( K ` { Y } ) )
30 snssg 
 |-  ( Y e. B -> ( Y e. ( K ` { Y } ) <-> { Y } C_ ( K ` { Y } ) ) )
31 30 biimpar 
 |-  ( ( Y e. B /\ { Y } C_ ( K ` { Y } ) ) -> Y e. ( K ` { Y } ) )
32 5 29 31 syl2anc 
 |-  ( ph -> Y e. ( K ` { Y } ) )
33 32 adantr 
 |-  ( ( ph /\ ( K ` { Y } ) C_ ( K ` { X } ) ) -> Y e. ( K ` { Y } ) )
34 26 33 sseldd 
 |-  ( ( ph /\ ( K ` { Y } ) C_ ( K ` { X } ) ) -> Y e. ( K ` { X } ) )
35 25 34 impbida 
 |-  ( ph -> ( Y e. ( K ` { X } ) <-> ( K ` { Y } ) C_ ( K ` { X } ) ) )
36 10 15 35 3bitr2d 
 |-  ( ph -> ( X .|| Y <-> ( K ` { Y } ) C_ ( K ` { X } ) ) )