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 ) )