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

Metamath Proof Explorer

Theorem lsmsnidl

Description: The product of the ring with a single element is a principal ideal. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypotheses lsmsnpridl.1 
|- B = ( Base ` R )
lsmsnpridl.2 
|- G = ( mulGrp ` R )
lsmsnpridl.3 
|- .X. = ( LSSum ` G )
lsmsnpridl.4 
|- K = ( RSpan ` R )
lsmsnpridl.5 
|- ( ph -> R e. Ring )
lsmsnpridl.6 
|- ( ph -> X e. B )
Assertion lsmsnidl 
|- ( ph -> ( B .X. { X } ) e. ( LPIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 lsmsnpridl.1 
 |-  B = ( Base ` R )
2 lsmsnpridl.2 
 |-  G = ( mulGrp ` R )
3 lsmsnpridl.3 
 |-  .X. = ( LSSum ` G )
4 lsmsnpridl.4 
 |-  K = ( RSpan ` R )
5 lsmsnpridl.5 
 |-  ( ph -> R e. Ring )
6 lsmsnpridl.6 
 |-  ( ph -> X e. B )
7 sneq 
 |-  ( y = X -> { y } = { X } )
8 7 fveq2d 
 |-  ( y = X -> ( K ` { y } ) = ( K ` { X } ) )
9 8 eqeq2d 
 |-  ( y = X -> ( ( B .X. { X } ) = ( K ` { y } ) <-> ( B .X. { X } ) = ( K ` { X } ) ) )
10 9 adantl 
 |-  ( ( ph /\ y = X ) -> ( ( B .X. { X } ) = ( K ` { y } ) <-> ( B .X. { X } ) = ( K ` { X } ) ) )
11 1 2 3 4 5 6 lsmsnpridl 
 |-  ( ph -> ( B .X. { X } ) = ( K ` { X } ) )
12 6 10 11 rspcedvd 
 |-  ( ph -> E. y e. B ( B .X. { X } ) = ( K ` { y } ) )
13 eqid 
 |-  ( LPIdeal ` R ) = ( LPIdeal ` R )
14 13 4 1 islpidl 
 |-  ( R e. Ring -> ( ( B .X. { X } ) e. ( LPIdeal ` R ) <-> E. y e. B ( B .X. { X } ) = ( K ` { y } ) ) )
15 5 14 syl 
 |-  ( ph -> ( ( B .X. { X } ) e. ( LPIdeal ` R ) <-> E. y e. B ( B .X. { X } ) = ( K ` { y } ) ) )
16 12 15 mpbird 
 |-  ( ph -> ( B .X. { X } ) e. ( LPIdeal ` R ) )