mnringmulrvald

Description: Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringmulrvald.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringmulrvald.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
	mnringmulrvald.3	⊢ ∙ = ( ._r ‘ 𝑅 )
	mnringmulrvald.4	⊢ 𝟎 = ( 0_g ‘ 𝑅 )
	mnringmulrvald.5	⊢ 𝐴 = ( Base ‘ 𝑀 )
	mnringmulrvald.6	⊢ + = ( +_g ‘ 𝑀 )
	mnringmulrvald.7	⊢ · = ( ._r ‘ 𝐹 )
	mnringmulrvald.8	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	mnringmulrvald.9	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
	mnringmulrvald.10	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	mnringmulrvald.11	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	mnringmulrvald	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnringmulrvald.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringmulrvald.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		mnringmulrvald.3	⊢ ∙ = ( ._r ‘ 𝑅 )
4		mnringmulrvald.4	⊢ 𝟎 = ( 0_g ‘ 𝑅 )
5		mnringmulrvald.5	⊢ 𝐴 = ( Base ‘ 𝑀 )
6		mnringmulrvald.6	⊢ + = ( +_g ‘ 𝑀 )
7		mnringmulrvald.7	⊢ · = ( ._r ‘ 𝐹 )
8		mnringmulrvald.8	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
9		mnringmulrvald.9	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
10		mnringmulrvald.10	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11		mnringmulrvald.11	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12	1 2 3 4 5 6 8 9	mnringmulrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) ) = ( ._r ‘ 𝐹 ) )
13	12 7	eqtr4di	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) ) = · )
14	13	eqcomd	⊢ ( 𝜑 → · = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) ) )
15		fveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 𝑎 ) = ( 𝑋 ‘ 𝑎 ) )
16		fveq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ‘ 𝑏 ) = ( 𝑌 ‘ 𝑏 ) )
17	15 16	oveqan12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) = ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) )
18	17	ifeq1d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) = if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) )
19	18	mpteq2dv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) ) = ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) )
20	19	mpoeq3dv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) ) ) = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) ) )
21	20	oveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) = ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) )
22	21	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ∙ ( 𝑦 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) = ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) )
23		ovexd	⊢ ( 𝜑 → ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) ∈ V )
24	14 22 10 11 23	ovmpod	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝐹 Σ_g ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) )

Metamath Proof Explorer

Theorem mnringmulrvald

Proof