Theorem idlsrgmulrval

Description: Value of the ring multiplication for the ideals of a ring R . (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	idlsrgmulrval.1	|- S = ( IDLsrg ` R )
	idlsrgmulrval.2	|- B = ( LIdeal ` R )
	idlsrgmulrval.3	|- .(x) = ( .r ` S )
	idlsrgmulrval.4	|- G = ( mulGrp ` R )
	idlsrgmulrval.5	|- .x. = ( LSSum ` G )
	idlsrgmulrval.6	|- ( ph -> R e. V )
	idlsrgmulrval.7	|- ( ph -> I e. B )
	idlsrgmulrval.8	|- ( ph -> J e. B )
Assertion	idlsrgmulrval	|- ( ph -> ( I .(x) J ) = ( ( RSpan ` R ) ` ( I .x. J ) ) )

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrval.1	|- S = ( IDLsrg ` R )
2		idlsrgmulrval.2	|- B = ( LIdeal ` R )
3		idlsrgmulrval.3	|- .(x) = ( .r ` S )
4		idlsrgmulrval.4	|- G = ( mulGrp ` R )
5		idlsrgmulrval.5	|- .x. = ( LSSum ` G )
6		idlsrgmulrval.6	|- ( ph -> R e. V )
7		idlsrgmulrval.7	|- ( ph -> I e. B )
8		idlsrgmulrval.8	|- ( ph -> J e. B )
9	1 2 4 5	idlsrgmulr	|- ( R e. V -> ( x e. B , y e. B |-> ( ( RSpan ` R ) ` ( x .x. y ) ) ) = ( .r ` S ) )
10	6 9	syl	|- ( ph -> ( x e. B , y e. B |-> ( ( RSpan ` R ) ` ( x .x. y ) ) ) = ( .r ` S ) )
11	3 10	eqtr4id	|- ( ph -> .(x) = ( x e. B , y e. B |-> ( ( RSpan ` R ) ` ( x .x. y ) ) ) )
12		oveq12	|- ( ( x = I /\ y = J ) -> ( x .x. y ) = ( I .x. J ) )
13	12	adantl	|- ( ( ph /\ ( x = I /\ y = J ) ) -> ( x .x. y ) = ( I .x. J ) )
14	13	fveq2d	|- ( ( ph /\ ( x = I /\ y = J ) ) -> ( ( RSpan ` R ) ` ( x .x. y ) ) = ( ( RSpan ` R ) ` ( I .x. J ) ) )
15		fvexd	|- ( ph -> ( ( RSpan ` R ) ` ( I .x. J ) ) e. _V )
16	11 14 7 8 15	ovmpod	|- ( ph -> ( I .(x) J ) = ( ( RSpan ` R ) ` ( I .x. J ) ) )