Metamath Proof Explorer

Theorem rspprop

Description: Properties of a class to be the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 30-Jun-2026)

Ref Expression
Hypotheses rspvalint.v 
|- B = ( Base ` R )
rspvalint.i 
|- I = ( LIdeal ` R )
rspvalint.k 
|- K = ( RSpan ` R )
Assertion rspprop 
|- ( ( R e. Ring /\ S C_ B ) -> ( ( K ` S ) = X <-> ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) )

Proof

Step Hyp Ref Expression
1 rspvalint.v 
 |-  B = ( Base ` R )
2 rspvalint.i 
 |-  I = ( LIdeal ` R )
3 rspvalint.k 
 |-  K = ( RSpan ` R )
4 3 1 2 rspcl 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( K ` S ) e. I )
5 3 1 rspssid 
 |-  ( ( R e. Ring /\ S C_ B ) -> S C_ ( K ` S ) )
6 3 2 rspssp 
 |-  ( ( R e. Ring /\ i e. I /\ S C_ i ) -> ( K ` S ) C_ i )
7 6 3expia 
 |-  ( ( R e. Ring /\ i e. I ) -> ( S C_ i -> ( K ` S ) C_ i ) )
8 7 ralrimiva 
 |-  ( R e. Ring -> A. i e. I ( S C_ i -> ( K ` S ) C_ i ) )
9 8 adantr 
 |-  ( ( R e. Ring /\ S C_ B ) -> A. i e. I ( S C_ i -> ( K ` S ) C_ i ) )
10 4 5 9 3jca 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( K ` S ) e. I /\ S C_ ( K ` S ) /\ A. i e. I ( S C_ i -> ( K ` S ) C_ i ) ) )
11 eleq1 
 |-  ( ( K ` S ) = X -> ( ( K ` S ) e. I <-> X e. I ) )
12 sseq2 
 |-  ( ( K ` S ) = X -> ( S C_ ( K ` S ) <-> S C_ X ) )
13 sseq1 
 |-  ( ( K ` S ) = X -> ( ( K ` S ) C_ i <-> X C_ i ) )
14 13 imbi2d 
 |-  ( ( K ` S ) = X -> ( ( S C_ i -> ( K ` S ) C_ i ) <-> ( S C_ i -> X C_ i ) ) )
15 14 ralbidv 
 |-  ( ( K ` S ) = X -> ( A. i e. I ( S C_ i -> ( K ` S ) C_ i ) <-> A. i e. I ( S C_ i -> X C_ i ) ) )
16 11 12 15 3anbi123d 
 |-  ( ( K ` S ) = X -> ( ( ( K ` S ) e. I /\ S C_ ( K ` S ) /\ A. i e. I ( S C_ i -> ( K ` S ) C_ i ) ) <-> ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) )
17 10 16 syl5ibcom 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( K ` S ) = X -> ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) )
18 3 2 rspssp 
 |-  ( ( R e. Ring /\ X e. I /\ S C_ X ) -> ( K ` S ) C_ X )
19 18 3adant3r3 
 |-  ( ( R e. Ring /\ ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) -> ( K ` S ) C_ X )
20 19 adantlr 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) -> ( K ` S ) C_ X )
21 ssint 
 |-  ( X C_ |^| { j e. I | S C_ j } <-> A. i e. { j e. I | S C_ j } X C_ i )
22 sseq2 
 |-  ( j = i -> ( S C_ j <-> S C_ i ) )
23 22 ralrab 
 |-  ( A. i e. { j e. I | S C_ j } X C_ i <-> A. i e. I ( S C_ i -> X C_ i ) )
24 21 23 sylbbr 
 |-  ( A. i e. I ( S C_ i -> X C_ i ) -> X C_ |^| { j e. I | S C_ j } )
25 24 3ad2ant3 
 |-  ( ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) -> X C_ |^| { j e. I | S C_ j } )
26 25 adantl 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) -> X C_ |^| { j e. I | S C_ j } )
27 1 2 3 rspvalint 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( K ` S ) = |^| { j e. I | S C_ j } )
28 27 adantr 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) -> ( K ` S ) = |^| { j e. I | S C_ j } )
29 26 28 sseqtrrd 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) -> X C_ ( K ` S ) )
30 20 29 eqssd 
 |-  ( ( ( R e. Ring /\ S C_ B ) /\ ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) -> ( K ` S ) = X )
31 30 ex 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) -> ( K ` S ) = X ) )
32 17 31 impbid 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( K ` S ) = X <-> ( X e. I /\ S C_ X /\ A. i e. I ( S C_ i -> X C_ i ) ) ) )