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	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrgmulrval.2	⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
	idlsrgmulrval.3	⊢ ⊗ = ( .r ‘ 𝑆 )
	idlsrgmulrval.4	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	idlsrgmulrval.5	⊢ · = ( LSSum ‘ 𝐺 )
	idlsrgmulrval.6	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	idlsrgmulrval.7	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
	idlsrgmulrval.8	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
Assertion	idlsrgmulrval	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) = ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 · 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrval.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
2		idlsrgmulrval.2	⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
3		idlsrgmulrval.3	⊢ ⊗ = ( .r ‘ 𝑆 )
4		idlsrgmulrval.4	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
5		idlsrgmulrval.5	⊢ · = ( LSSum ‘ 𝐺 )
6		idlsrgmulrval.6	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
7		idlsrgmulrval.7	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
8		idlsrgmulrval.8	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
9	1 2 4 5	idlsrgmulr	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) ) = ( .r ‘ 𝑆 ) )
10	6 9	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) ) = ( .r ‘ 𝑆 ) )
11	3 10	eqtr4id	⊢ ( 𝜑 → ⊗ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) ) )
12		oveq12	⊢ ( ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) → ( 𝑥 · 𝑦 ) = ( 𝐼 · 𝐽 ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) → ( 𝑥 · 𝑦 ) = ( 𝐼 · 𝐽 ) )
14	13	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 · 𝐽 ) ) )
15		fvexd	⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 · 𝐽 ) ) ∈ V )
16	11 14 7 8 15	ovmpod	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) = ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 · 𝐽 ) ) )