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		mulridx	⊢ .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 ‘ 𝐹 ) )