Metamath Proof Explorer

Theorem rspsn0

Description: A principal ideal (an ideal generated by one element) in a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 12-Jul-2026)

Ref Expression
Hypotheses elrspsn.1 
|- B = ( Base ` R )
elrspsn.2 
|- .x. = ( .r ` R )
elrspsn.3 
|- K = ( RSpan ` R )
Assertion rspsn0 
|- ( ( R e. Ring /\ X e. B ) -> ( K ` { X } ) = { i e. B | E. x e. B i = ( x .x. X ) } )

Proof

Step Hyp Ref Expression
1 elrspsn.1 
 |-  B = ( Base ` R )
2 elrspsn.2 
 |-  .x. = ( .r ` R )
3 elrspsn.3 
 |-  K = ( RSpan ` R )
4 1 2 3 elrspsn 
 |-  ( ( R e. Ring /\ X e. B ) -> ( i e. ( K ` { X } ) <-> E. x e. B i = ( x .x. X ) ) )
5 simpll 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ x e. B ) -> R e. Ring )
6 simpr 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ x e. B ) -> x e. B )
7 simplr 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ x e. B ) -> X e. B )
8 1 2 5 6 7 ringcld 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ x e. B ) -> ( x .x. X ) e. B )
9 eleq1 
 |-  ( i = ( x .x. X ) -> ( i e. B <-> ( x .x. X ) e. B ) )
10 8 9 syl5ibrcom 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ x e. B ) -> ( i = ( x .x. X ) -> i e. B ) )
11 10 rexlimdva 
 |-  ( ( R e. Ring /\ X e. B ) -> ( E. x e. B i = ( x .x. X ) -> i e. B ) )
12 11 pm4.71rd 
 |-  ( ( R e. Ring /\ X e. B ) -> ( E. x e. B i = ( x .x. X ) <-> ( i e. B /\ E. x e. B i = ( x .x. X ) ) ) )
13 4 12 bitrd 
 |-  ( ( R e. Ring /\ X e. B ) -> ( i e. ( K ` { X } ) <-> ( i e. B /\ E. x e. B i = ( x .x. X ) ) ) )
14 rabid 
 |-  ( i e. { i e. B | E. x e. B i = ( x .x. X ) } <-> ( i e. B /\ E. x e. B i = ( x .x. X ) ) )
15 13 14 bitr4di 
 |-  ( ( R e. Ring /\ X e. B ) -> ( i e. ( K ` { X } ) <-> i e. { i e. B | E. x e. B i = ( x .x. X ) } ) )
16 15 alrimiv 
 |-  ( ( R e. Ring /\ X e. B ) -> A. i ( i e. ( K ` { X } ) <-> i e. { i e. B | E. x e. B i = ( x .x. X ) } ) )
17 nfcv 
 |-  F/_ i ( K ` { X } )
18 nfrab1 
 |-  F/_ i { i e. B | E. x e. B i = ( x .x. X ) }
19 17 18 cleqf 
 |-  ( ( K ` { X } ) = { i e. B | E. x e. B i = ( x .x. X ) } <-> A. i ( i e. ( K ` { X } ) <-> i e. { i e. B | E. x e. B i = ( x .x. X ) } ) )
20 16 19 sylibr 
 |-  ( ( R e. Ring /\ X e. B ) -> ( K ` { X } ) = { i e. B | E. x e. B i = ( x .x. X ) } )