Theorem lsmsnpridl

Description: The product of the ring with a single element is equal to the principal ideal generated by that element. (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	lsmsnpridl	|- ( ph -> ( B .X. { X } ) = ( K ` { X } ) )

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	2 1	mgpbas	|- B = ( Base ` G )
8		eqid	|- ( .r ` R ) = ( .r ` R )
9	2 8	mgpplusg	|- ( .r ` R ) = ( +g ` G )
10	2	fvexi	|- G e. _V
11	10	a1i	|- ( ph -> G e. _V )
12		ssidd	|- ( ph -> B C_ B )
13	7 9 3 11 12 6	elgrplsmsn	|- ( ph -> ( x e. ( B .X. { X } ) <-> E. y e. B x = ( y ( .r ` R ) X ) ) )
14	1 8 4	rspsnel	|- ( ( R e. Ring /\ X e. B ) -> ( x e. ( K ` { X } ) <-> E. y e. B x = ( y ( .r ` R ) X ) ) )
15	5 6 14	syl2anc	|- ( ph -> ( x e. ( K ` { X } ) <-> E. y e. B x = ( y ( .r ` R ) X ) ) )
16	13 15	bitr4d	|- ( ph -> ( x e. ( B .X. { X } ) <-> x e. ( K ` { X } ) ) )
17	16	eqrdv	|- ( ph -> ( B .X. { X } ) = ( K ` { X } ) )