Metamath Proof Explorer

Theorem 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 ⊢ 𝟎 = ( 0g ‘ 𝑅 )
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 ⊢ 𝟎 = ( 0g ‘ 𝑅 )
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 ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑋 ‘ 𝑎 ) ∙ ( 𝑌 ‘ 𝑏 ) ) , 𝟎 ) ) ) ) )