Metamath Proof Explorer

Theorem mnringmulrd

Description: The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses mnringmulrd.1 ⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
mnringmulrd.2 ⊢ 𝐵 = ( Base ‘ 𝐹 )
mnringmulrd.3 ⊢ · = ( .r ‘ 𝑅 )
mnringmulrd.4 ⊢ 0 = ( 0g ‘ 𝑅 )
mnringmulrd.5 ⊢ 𝐴 = ( Base ‘ 𝑀 )
mnringmulrd.6 ⊢ + = ( +g ‘ 𝑀 )
mnringmulrd.7 ⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
mnringmulrd.8 ⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
Assertion mnringmulrd ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝐹 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) = ( .r ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 mnringmulrd.1 ⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2 mnringmulrd.2 ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 mnringmulrd.3 ⊢ · = ( .r ‘ 𝑅 )
4 mnringmulrd.4 ⊢ 0 = ( 0g ‘ 𝑅 )
5 mnringmulrd.5 ⊢ 𝐴 = ( Base ‘ 𝑀 )
6 mnringmulrd.6 ⊢ + = ( +g ‘ 𝑀 )
7 mnringmulrd.7 ⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
8 mnringmulrd.8 ⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
9 eqid ⊢ ( 𝑅 freeLMod 𝐴 ) = ( 𝑅 freeLMod 𝐴 )
10 1 2 5 9 7 8 mnringbaserd ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) )
11 5 fvexi ⊢ 𝐴 ∈ V
12 11 11 mpoex ⊢ ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ∈ V
13 12 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ∈ V )
14 1 ovexi ⊢ 𝐹 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝐹 ∈ V )
16 ovex ⊢ ( 𝑅 freeLMod 𝐴 ) ∈ V
17 16 a1i ⊢ ( 𝜑 → ( 𝑅 freeLMod 𝐴 ) ∈ V )
18 2 10 eqtr3id ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) )
19 1 5 9 7 8 mnringaddgd ⊢ ( 𝜑 → ( +g ‘ ( 𝑅 freeLMod 𝐴 ) ) = ( +g ‘ 𝐹 ) )
20 19 eqcomd ⊢ ( 𝜑 → ( +g ‘ 𝐹 ) = ( +g ‘ ( 𝑅 freeLMod 𝐴 ) ) )
21 13 15 17 18 20 gsumpropd ⊢ ( 𝜑 → ( 𝐹 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) = ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) )
22 10 10 21 mpoeq123dv ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝐹 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) = ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) )
23 fvex ⊢ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ∈ V
24 23 23 mpoex ⊢ ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ∈ V
25 mulrid ⊢ .r = Slot ( .r ‘ ndx )
26 25 setsid ⊢ ( ( ( 𝑅 freeLMod 𝐴 ) ∈ V ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ∈ V ) → ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) = ( .r ‘ ( ( 𝑅 freeLMod 𝐴 ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) ) )
27 16 24 26 mp2an ⊢ ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) = ( .r ‘ ( ( 𝑅 freeLMod 𝐴 ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )
28 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐴 ) )
29 1 3 4 5 6 9 28 7 8 mnringvald ⊢ ( 𝜑 → 𝐹 = ( ( 𝑅 freeLMod 𝐴 ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )
30 29 fveq2d ⊢ ( 𝜑 → ( .r ‘ 𝐹 ) = ( .r ‘ ( ( 𝑅 freeLMod 𝐴 ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) ) )
31 27 30 eqtr4id ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) , 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↦ ( ( 𝑅 freeLMod 𝐴 ) Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) = ( .r ‘ 𝐹 ) )
32 22 31 eqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝐹 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) = ( .r ‘ 𝐹 ) )