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	No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
	idlsrgmulrval.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
	idlsrgmulrval.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
	idlsrgmulrval.4	$$⊢G={\mathrm{mulGrp}}_R$$
	idlsrgmulrval.5	$$⊢\underset{\dot{}}{·}=\mathrm{LSSum}\left(G\right)$$
	idlsrgmulrval.6	$$⊢\phi \to R\in V$$
	idlsrgmulrval.7	$$⊢\phi \to I\in B$$
	idlsrgmulrval.8	$$⊢\phi \to J\in B$$
Assertion	idlsrgmulrval	$$⊢\phi \to I\underset{\dot{}}{\otimes }J=\mathrm{RSpan}\left(R\right)\left(I\underset{\dot{}}{·}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrval.1	Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
2		idlsrgmulrval.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
3		idlsrgmulrval.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
4		idlsrgmulrval.4	$$⊢G={\mathrm{mulGrp}}_R$$
5		idlsrgmulrval.5	$$⊢\underset{\dot{}}{·}=\mathrm{LSSum}\left(G\right)$$
6		idlsrgmulrval.6	$$⊢\phi \to R\in V$$
7		idlsrgmulrval.7	$$⊢\phi \to I\in B$$
8		idlsrgmulrval.8	$$⊢\phi \to J\in B$$
9	1 2 4 5	idlsrgmulr	$$⊢R\in V\to \left(x\in B,y\in B⟼\mathrm{RSpan}\left(R\right)\left(x\underset{\dot{}}{·}y\right)\right)={\cdot }_S$$
10	6 9	syl	$$⊢\phi \to \left(x\in B,y\in B⟼\mathrm{RSpan}\left(R\right)\left(x\underset{\dot{}}{·}y\right)\right)={\cdot }_S$$
11	3 10	eqtr4id	$$⊢\phi \to \underset{\dot{}}{\otimes }=\left(x\in B,y\in B⟼\mathrm{RSpan}\left(R\right)\left(x\underset{\dot{}}{·}y\right)\right)$$
12		oveq12	$$⊢\left(x=I\wedge y=J\right)\to x\underset{\dot{}}{·}y=I\underset{\dot{}}{·}J$$
13	12	adantl	$$⊢\left(\phi \wedge \left(x=I\wedge y=J\right)\right)\to x\underset{\dot{}}{·}y=I\underset{\dot{}}{·}J$$
14	13	fveq2d	$$⊢\left(\phi \wedge \left(x=I\wedge y=J\right)\right)\to \mathrm{RSpan}\left(R\right)\left(x\underset{\dot{}}{·}y\right)=\mathrm{RSpan}\left(R\right)\left(I\underset{\dot{}}{·}J\right)$$
15		fvexd	$$⊢\phi \to \mathrm{RSpan}\left(R\right)\left(I\underset{\dot{}}{·}J\right)\in \mathrm{V}$$
16	11 14 7 8 15	ovmpod	$$⊢\phi \to I\underset{\dot{}}{\otimes }J=\mathrm{RSpan}\left(R\right)\left(I\underset{\dot{}}{·}J\right)$$